*To*: Lee Martin CCNP <tesleft at hotmail.com>*Subject*: Re: [isabelle] what is the correct syntax to do simple auto prove proposition*From*: Makarius <makarius at sketis.net>*Date*: Wed, 28 May 2014 15:48:25 +0200 (CEST)*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BAY178-W13AFF4CEC3B43FC6755DA0B63A0@phx.gbl>*References*: <BAY178-W132669A0B0DF8D14AEAD6CB63B0@phx.gbl>, <922E7845-0465-44A0-9FCA-960F246D2ACE@gmail.com> <BAY178-W13AFF4CEC3B43FC6755DA0B63A0@phx.gbl>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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.

Moreover, can you say what this produces in the Output window? ML {* getenv "USER_HOME"; getenv "ISABELLE_HOME"; getenv "ISABELLE_HOME_USER" *}

Makarius

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

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

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

- Previous by Date: [isabelle] jEdit 5.2pre1
- Next by Date: [isabelle] How to use transfer when lifting_forget has been called ?
- Previous by Thread: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Next by Thread: [isabelle] Rational functions
- 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