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



Hi Jasmin,
in window 8, i open Isabelle2013-2.exe 
it return error
[line 1 of "$ISABELLE_HOME_USER/etc/preferences"] error: bad input
ini file do not have this path
then i open cygwin-terminal.bat and click Isabelle2013-2.exe again, still got error
in cygwin-terminal.bat i type ./Isabelle2013-2.exe got the same error too.
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.