[isabelle-dev] Isabelle/jEdit: non-trivial theory merge

Lars Noschinski noschinl at in.tum.de
Wed Mar 7 14:24:31 CET 2012


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)))"


   Attempt to perform non-trivial merge of theories:
   {..., Relation, Transitive_Closure, Partial_Function, Wellfounded, 
   {..., 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