*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Proof mode still on after failed by (Isabelle 2013-RC2)*From*: Joachim Breitner <breitner at kit.edu>*Date*: Mon, 04 Feb 2013 14:52:05 +0100

Hi, 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 end works fine, i.e. despite the "by" command failing to prove the lemma, Isabelle still accepts the following "lemma" command. So "by" managed to switch from proof mode to theory mode. This is good and important for non-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 end the "lemma" command is now under-wiggled and shows the error message “Illegal application of command "lemma" in proof mode”. I was expecting the same behavior as above. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] afp_build in RC2
- Previous by Thread: Re: [isabelle] Unexpected Behavior with Sum_Type
- Next by Thread: Re: [isabelle] Proof mode still on after failed by (Isabelle 2013-RC2)
- 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