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.