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.
Andreas
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
