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

[Andreas Lochbihler]

Dear all,


In the attachment, there's an example.

Best,
Andreas

in Isabelle abd760a19e22, 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.

Scratch.thy
Description: application/extension-thy

ScratchA.thy
Description: application/extension-thy

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev