[isabelle-dev] Isabelle/jEdit: non-trivial theory merge
Lars Noschinski
noschinl at in.tum.de
Wed Mar 7 14:24:31 CET 2012
Hi,
today (57bf0cecb366) I noticed some strange behaviour in jEdit when
bootstrapping HOL. I had HOL fully loaded (after working around the
usual problems with newly defined commands). However, every change which
causes FunDef.thy to be reprocessed, triggered error in later theories
using the "fun" or "function" commands:
For example, Divide.thy at line 1194:
function posDivAlg :: "int ⇒ int ⇒ int × int" where
"posDivAlg a b = (if a < b ∨ b ≤ 0 then (0, a)
else adjust b (posDivAlg a (2 * b)))"
with
Attempt to perform non-trivial merge of theories:
{..., Relation, Transitive_Closure, Partial_Function, Wellfounded,
FunDef:33}
{..., Equiv_Relations, Int, Nat_Numeral, Nat_Transfer, Divides:408}
When I reload Divide.thy, this problem goes away. Similar problems occur
at other uses of "function" in later theories.
I recall that I was able to do changes in early HOL without such
problems with jEdit some months ago.
-- Lars
More information about the isabelle-dev
mailing list