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

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

[isabelle-dev] problem with the proof recording

Dear All, this refers to 3fbcfa911863. If I use the proof recording, processing of the following theory takes infinite time: theory Problem imports Main begin lemma list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P) apply (simp add: fun_eq_iff list_all2_def list_all_iff