[isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
Yes indeed it helps - still I don't understand the behavior, but I can
go on with my proof!
Thanks a lot
On Wed, Sep 9, 2009 at 9:53 AM, Florian
Haftmann<florian.haftmann at informatik.tu-muenchen.de> wrote:
> 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 ..
> assume True show "C u u" sorry
> Hope this helps
This archive was generated by a fusion of
Pipermail (Mailman edition) and