[isabelle-dev] including raises Attempt to perform non-trivial merge of theories
makarius at sketis.net
Mon Sep 2 12:56:37 CEST 2013
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?
More information about the isabelle-dev