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

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.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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