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 in.tum.de>
> 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

    $AFP

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.