# Re: [isabelle] what is the correct syntax to do simple auto prove proposition

Hi Jasmin,
after try in ubuntu, and press apply , it is like loading, no output or response show.
How to use it correctly?
Regards,
Martin
> From: jasmin.blanchette at gmail.com
> Date: Mon, 26 May 2014 13:53:58 +0200
> To: tesleft at hotmail.com
> CC: isabelle-users at cl.cam.ac.uk
> Subject: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
>
> 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
>
>

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