| #
529218cb |
|
19-Oct-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Tweak genUseScript to work when generating prefix to boolScript
|
| #
fc989ab8 |
|
24-Feb-2019 |
Michael Norrish <michael.norrish@nicta.com.au> |
Get developers/genUseScript to build again
|
| #
f032d2b3 |
|
14-Nov-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix genUseScript to work with recent HOL changes
|
| #
86b3eae0 |
|
21-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Complete basic Poly implementation of TheoryIO (separate dat files)
Still to tweak Holmake and to make sure it all works on Moscow ML
|
| #
9868a84b |
|
07-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix genUseScript given holpathdb changes ($(HOLDIR) in .uo files)
|
| #
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).
|