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 (also attached).
(You do need to have src/TeX/holtexbasic.sty in your TeX input path, which is
often easily accomplished by copying it into your current directory.)
The behaviour on larger data types is tested in the directory
src/TeX/theory_tests, but if you find a situation where the printing seems
sub-par, please report it.
Best wishes,
Michael
On 02/06/14 01:43, Ramana Kumar wrote:
> 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 print a pretty datatype
> definition using the EmitTeX munger (or a pointer to said instructions).
>
> Cheers,
> Ramana
foo.pdf
Description: Adobe PDF document
\documentclass{article}
\usepackage{alltt}
\usepackage{holtexbasic}
\begin{document}
\noindent This is a ``pretty'' datatype declaration for the list type
\begin{alltt}
\HOLthm[>>10]{list.datatype_list}
\end{alltt}
\end{document}
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/NeoTech
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
