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



Hi Sigurd,

in "show" statements you should refrain from using the plain metalogic
connectives ==> and !! -- they are used by the Isar framework;  the
solution is to internalize ==> and !! into proper Isar text (assume for
==>, fix for !!), as follows:

definition "C a b \<longleftrightarrow> b < a"

lemma a:
shows "C u u \<Longrightarrow> True"
  and "True \<Longrightarrow> C u u"
proof -
  assume "C u u" show True ..
next
  assume True show "C u u" sorry
qed

Hope this helps
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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