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



On Tue, 27 May 2014, Lee Martin CCNP wrote:

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.

It is hard to guess from a distance. Maybe something is just wrong with your local Isabelle installation.

When you start the main exe, do you get the Isabelle/jEdit application with the prover running, and giving feedback on your theory? You can try that quickly by the Documentation panel, with the Examples at the bottom. There should be some flashing of colors when you open src/HOL/ex/Seq.thy for example.


Moreover, can you say what this produces in the Output window?

 ML {* getenv "USER_HOME"; getenv "ISABELLE_HOME"; getenv "ISABELLE_HOME_USER" *}

Again this needs to be a proper theory file with theory header, e.g. the body of one of the examples (without saving the changed file).


	Makarius




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