[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 ..
> next
>  assume True show "C u u" sorry
> qed
>
> Hope this helps
>        Florian
>
>





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