*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] proof statement fails*From*: Gergely Buday <gbuday at gmail.com>*Date*: Sat, 7 Jul 2012 08:51:41 +0200

Hi, I have written theory Let imports Main begin lemma "(2 :: nat) + 2 = 4" proof Now, 'proof' results in "empty result sequence -- proof command failed" Otherwise, i.e. without Isar, apply (auto) finishes the proof, so the lemma itself is well-written. What else could fail? - Gergely

**Follow-Ups**:**Re: [isabelle] proof statement fails***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] HOLCF equality
- Next by Date: Re: [isabelle] proof statement fails
- Previous by Thread: Re: [isabelle] HOLCF equality type class
- Next by Thread: Re: [isabelle] proof statement fails
- Cl-isabelle-users July 2012 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