[isabelle] Bug in assumption display



Dear Isabelle users,

I have just upgraded my (Ubuntu) emacs to 22.2.1
and see the following funny behaviour:

lemma "[| A; B |] ==> A"

yields:

goal (1 subgoal):
 1. A ==> B ==> A

with ProofGeneral 3.7.1 (advertised as latest stable),
while starting the command line "isabelle -I" gives (correctly):

> lemma "[| A; B |] ==> A";
proof (prove): step 0

goal (1 subgoal):
 1. [| A; B |] ==> A

XSymbols and everything else seems to be working properly,
I also re-byte-compiled ProofGeneral.

Has any of you encountered a similar problem?

Thanks,

	Holger





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