*To*: Lee Martin CCNP <tesleft at hotmail.com>*Subject*: Re: [isabelle] what is the correct syntax to do simple auto prove proposition*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Mon, 26 May 2014 13:53:58 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BAY178-W132669A0B0DF8D14AEAD6CB63B0@phx.gbl>*References*: <BAY178-W132669A0B0DF8D14AEAD6CB63B0@phx.gbl>

Hi Martin, Am 26.05.2014 um 05:22 schrieb Lee Martin CCNP <tesleft at hotmail.com>: > Hi sir, > After choose sledgerhammer, and check isar proof and click Apply, got error > what is the correct syntax to prove simple proposition > Illegal application of command "lemma" at top level > lemma "(a ∨ b) ∧ (b ∨ c) --> (a ∨ c)"apply autodone Is this your entire theory file? If so, you will need to start with the usual header. Assuming your theory file is called Foo.thy, this means: theory Foo imports Main begin This should be explained in the tutorials (the first two bullet points at http://isabelle.in.tum.de/documentation.html). Regards, Jasmin

**Follow-Ups**:**Re: [isabelle] what is the correct syntax to do simple auto prove proposition***From:*Lee Martin CCNP

**References**:**[isabelle] what is the correct syntax to do simple auto prove proposition***From:*Lee Martin CCNP

- Previous by Date: [isabelle] what is the correct syntax to do simple auto prove proposition
- Next by Date: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Previous by Thread: [isabelle] what is the correct syntax to do simple auto prove proposition
- Next by Thread: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Cl-isabelle-users May 2014 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