#
992441ba |
|
24-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Tool to generate use-scripts for early HOL For example, developers/genUseScript --hol src/bool/boolScript.sml > usethis.ML poly --use usethis.ML sets up an interactive session with all of the kernel up to but not including boolScript.sml (no pretty-printing enabled, or other interactive niceties though).
|