The default method to do this hasn't changed, and the repository version of HOL
will print type declarations with the new style. Thus the command
$ ~/HOL/bin/mkmunge
$ ./munge.exe < foo.htex > foo.tex
$ pdflatex foo.tex
will produce the attached foo.pdf, when given the file foo.htex
CALL FOR PARTICIPATION
**ITRS 2014**
7th Workshop on Intersection Types and Related Systems
Vienna, Austria, July 18th, 2014
http://vsl2014.at/meeti
Dear HOL users,
I have found the book by Brian T. Graham about a formalisation of an
SECD microprocessor using the HOL proof assistant.
I have not found the proof script. Do you know whether it is
proprietary or available for research purposes?
- Gergely
Hi all,
I suspect there's a nice way to get the munger to print datatypes in the
syntax accepted by the new Datatype command (i.e. without all the "of"s,
and perhaps with better line-breaking), but I can't figure it out right
now. Does anyone know?
Ideally I'm looking for instructions for how to
