(twice). An example is attached showing this. I have reduced
this as far as I can but still a few small library files are required.
The file 'polyml.sml' is the top-level file that uses the other files.
Regards,
Phil
polyml_compiler_issue-20150922-1.tar.gz
Description: GNU Zip compressed data
It would be useful for HOL4 if polyc could be used with a different base
executable. At the moment, the shell-script is hardcoded to use e.g.,
/usr/local/bin/poly. If HOL has created a different heap H with a lot of
preloaded context, but for which the main function is still