[isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".



It seems that sometimes it is not enough to show all goals for qed to
finish the proof.

The smallest example I have been able to make is the following (the
lemma is not true, but because of "sorry" it should be accepted
anyways.)

In proof general all lines before qed are accepted, but when I try
next-step, it gives me: *** Failed to finish proof
*** At command "qed".

theory T
imports Main
begin

definition "C a b ≡ b < a"

lemma a:
shows "⟦C u u⟧ ⟹ True"
  and "⟦True⟧ ⟹ C u u"
proof -
  show "⟦C u u⟧ ⟹ True"
    sorry
  show "⟦True⟧ ⟹ C u u"
    sorry
qed

end

I hope somebody sees what I or Isabelle is doing wrong ;)

Sigurd





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