*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] Proof mode still on after failed by (Isabelle 2013-RC2)*From*: Makarius <makarius at sketis.net>*Date*: Mon, 11 Feb 2013 17:07:23 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1359985925.9352.13.camel@kirk>*References*: <1359985925.9352.13.camel@kirk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 4 Feb 2013, Joachim Breitner wrote:

I installed 2013-RC2 to play around and see what has changed, and found this issue: theory Scratch imports Main begin lemma "True" by (rule conjI) lemma "True ∨ True" sorry endworks fine, i.e. despite the "by" command failing to prove the lemma,Isabelle still accepts the following "lemma" command. So "by" managed toswitch from proof mode to theory mode. This is good and important fornon-linear proof editing.

But this does not work reliably. With just a small small change, such as giving the lemma a name: theory Scratch imports Main begin lemma name: "True" by (rule conjI) lemma "True ∨ True" sorry endthe "lemma" command is now under-wiggled and shows the error message“Illegal application of command "lemma" in proof mode”. I was expectingthe same behavior as above.

Makarius

**References**:**[isabelle] Proof mode still on after failed by (Isabelle 2013-RC2)***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Unexpected Behavior with Sum_Type
- Next by Date: Re: [isabelle] Generating .tex from .thy without a proper session
- Previous by Thread: [isabelle] Proof mode still on after failed by (Isabelle 2013-RC2)
- Next by Thread: [isabelle] MetiTarski 2.1 released!
- Cl-isabelle-users February 2013 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