*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".*From*: Sigurd Torkel Meldgaard <stm at cs.au.dk>*Date*: Wed, 9 Sep 2009 10:42:37 +0200*In-reply-to*: <392528d30909090136l417e04c5t4777c37b8d7780e1@mail.gmail.com>*References*: <392528d30909080733k75c9bebeib350047fc82a3d46@mail.gmail.com> <4AA75EFC.60201@informatik.tu-muenchen.de> <392528d30909090136l417e04c5t4777c37b8d7780e1@mail.gmail.com>*Sender*: yogurth at gmail.com

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 > >

**References**:**[isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".***From:*Sigurd Torkel Meldgaard

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

- Previous by Date: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Next by Date: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Previous by Thread: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Next by Thread: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list