*To*: Sigurd Torkel Meldgaard <stm at cs.au.dk>*Subject*: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 09 Sep 2009 09:53:32 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <392528d30909080733k75c9bebeib350047fc82a3d46@mail.gmail.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <392528d30909080733k75c9bebeib350047fc82a3d46@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

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

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

- Previous by Date: Re: [isabelle] Existential Quantifiers
- Next by Date: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Previous by Thread: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Next by Thread: [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