# [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.*