[isabelle] Isabelle/Isar crash



Hello all,

I'm trying to load a very large lemma, but this does not succeed. I get the error message

gc.c:2553: failed assertion `A.I.updated == A.I.i_marked + A.M.i_marked - immutable_overflow' /Volumes/Heart/Users/rauch/Applications/Isabelle2005/lib/scripts/run- polyml: line 126: 7112 Abort trap "$POLY" $ML_OPTIONS "$ (fixpath "$DB")"

in the *isabelle/isar* window and  the message

Process isabelle/isar exited abnormally with code 134

in XEmacs (this is Isabelle 2005 on Mac OS X).

Is this a known problem? Is the lemma too large?

I can send an image + a short theory (or alternatively a larger bunch of theories) if anybody is interested.

Thanks in advance for any help

Nicole







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.