Re: [isabelle] Bug in assumption display



I think the standard behavior is to prefer `[| A; B |] ==> A' over
`A ==> B ==> A' for output. But I would not consider it a bug, if it is done the other way round (since both formulas are logically equivalent). I can't believe, however, that output behavior depends on the emacs version. I think you just have a different Isabelle or ProofGeneral version.

cheers

christian

Holger Gast wrote:
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.