Thanks for the question Heiko.
I think Thomas’s answer is the best that can be done at the moment, but now
that I’m aware of the problem, I will adjust polyscripter to pay attention to
`INCLUDES =` lines in a Holmakefile, and perhaps also `-I` command-line options
passed to polyscripter.
With
Hi Heiko,
you need to load the theory before you can open it. Usually you don't
need to take care of it yourself, because tools like Holmake or the
emacs mode take care of it for you. However, for polyscripter you need a
line like
>>__ load "aTheory"
before you can open it. Often you want to loa
Hello everyone,
I am trying to use the polyscripter tool to generate some nice output
from my HOL4 definitions.
In my directory, I have a file aScript.sml with theorem b_def being
produced. After compiling with Holmake, I have the files aTheory.sml and
aTheory.sig, where aTheory.sig contain
