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
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
On Mon, 19 Aug 2013, Makarius wrote:
After two rounds of looking through it, I've devised the included change. It
seems to address the situation exposed by Andreas, but breaks
HOL/Quotient_Examples.thy here:
lift_definition fmember :: 'a ⇒ 'a fset ⇒ bool (infix |∈| 50) is λx
xs. x ∈ set xs
On Wed, 14 Aug 2013, Ondřej Kunčar wrote:
On 08/13/2013 04:19 PM, Andreas Lochbihler wrote:
Dear all,
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.
In the attachment,
Dear all,
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.
In the attachment, there's an example.
Best,
Andreas
Scratch.thy
Description: application/extension-thy
