*To*: Holger Gast <gast at informatik.uni-tuebingen.de>*Subject*: Re: [isabelle] Bug in assumption display*From*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Date*: Tue, 20 Jan 2009 09:37:06 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <49749D0F.3040108@informatik.uni-tuebingen.de>*References*: <49749D0F.3040108@informatik.uni-tuebingen.de>*User-agent*: Thunderbird 2.0.0.19 (X11/20090105)

I think the standard behavior is to prefer `[| A; B |] ==> A' over

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

**References**:**[isabelle] Bug in assumption display***From:*Holger Gast

- Previous by Date: Re: [isabelle] Isar tutorial example broken?
- Next by Date: Re: [isabelle] Isar tutorial example broken?
- Previous by Thread: [isabelle] Bug in assumption display
- Next by Thread: Re: [isabelle] Bug in assumption display
- Cl-isabelle-users January 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list