Re: [isabelle] Issue with `Simpl` user guide `Fac` example



On Sat, 19 Apr 2014, Lars Noschinski wrote:

On 18.04.2014 23:23, Yannick Duchêne (Hibou57) wrote:

You're right, I checked it works (I initially did without -d, after a
thread on the StackOverflow forum). I will edit my Isabelle jEdit
launcher to always have this -d option, as it seems it does not disallow
the use of other heap images, like HOL.

You can also add the line

   $AFP

to a file name ROOTS in $ISABELLE_HOME_USER (i.e. ~/.isabelle/ on Unix).

Using a ROOTS file in the proper place is indeed the standard way these days, although that is little known.

Note that $ISABELLE_HOME_USER above only works for unnamed repository versions. Luckily Isabelle/jEdit already knows $ISABELLE_HOME and $ISABELLE_HOME_USER in the file browser, so these symbolic names are univerally accepted (even on Windows in that notation).


	Makarius


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