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 contains the theorem b_def as expected.
I am trying to produce a pretty-printed version of b_def in a file c.txt
that contains the following two lines:
>>__ open aTheory
##thm b_def
However, running $HOL_DIR/Manual/Tools/polyscripter < c.txt gives me an
error in the line with open aTheory, that aTheory has not been declared.
Putting
>> OS.FileSys.getDir()
will print the working directory I am in at the moment.
Can someone explain to me how to set up my files such that I can
reference other theories using polyscripter?
Thanks in advance,
Heiko
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
