[isabelle] Proof mode still on after failed by (Isabelle 2013-RC2)



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
Description: This is a digitally signed message part



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