Re: [isabelle] Issue with `Simpl` user guide `Fac` example
Le Fri, 18 Apr 2014 21:50:41 +0200, Lars Noschinski
<noschinl at in.tum.de> a écrit:
On 18.04.2014 03:22, Yannick Duchêne (Hibou57) wrote:
Also, a question aside: is it mandatory to import `$AFP/Simpl/Simpl`? It
takes long to load for me, near to ten minutes. Is there an alternative
Just start from the Simpl session image, then you only have to wait once.
isabelle -d '$AFP' -l Simpl
should do the trick.
Hi Lars, and thanks for your care,
That's what I first did, I built an image, but it did not show up in the
jEdit theories list and launching Isabelle from the command line with the
`-l` option, thrown a dialogue complaining the cession was not
found: “Undefined session(s): "Simpl"”. I've checked the heap image was
built in the same directory as others (along with HOL, HOL-BNF and and
al). As far as I can tell, Isabelle was properly configured for the use of
the AFP (path specified in `~/.isabelle/etc/components`).
I have not investigated this issue further, as I'm busy reading the
`Imperative_HOL` theory source files for now.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and