[isabelle-dev] including raises Attempt to perform non-trivial merge of theories

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Mon Sep 2 13:23:36 CEST 2013

Hi Makarius,

The error has already gone away in cb82606b8215 when Ondřej moved all the Quotient_... 
theories to Main, i.e., there was no non-trivial merge necessary any more. My concrete 
application works as expected at the moment.


On 02/09/13 12:56, Makarius wrote:
> On Tue, 13 Aug 2013, Andreas Lochbihler wrote:
>> I get the error "Attempt to perform non-trivial merge of theories" when I include a
>> bundle from another theory and there are at least two imports. In the attachment,
>> there's an example.
> This should work in Isabelle/ef65d5ee60cf.  Are there any remaining problems in the
> concrete application behind the example?
>      Makarius

More information about the isabelle-dev mailing list