[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
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".
definition "C a b ≡ b < a"
shows "⟦C u u⟧ ⟹ True"
and "⟦True⟧ ⟹ C u u"
show "⟦C u u⟧ ⟹ True"
show "⟦True⟧ ⟹ C u u"
I hope somebody sees what I or Isabelle is doing wrong ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and