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

On 18.04.2014 23:23, Yannick Duchêne (Hibou57) wrote:
> Le Fri, 18 Apr 2014 22:17:58 +0200, Lars Noschinski <noschinl at>
> a écrit:
>> Since some time, the '-l' parameter does not specify a logic image
>> anymore, but a session. Even if you have the AFP configured as a
>> component, you need to pass "-d '$AFP'" to tell the session where the
>> Simpl session is found.
>>   -- Lars
> 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


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

Attachment: signature.asc
Description: OpenPGP digital signature

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