Hi there, I've just tried this out. The latest Git checkout seems to work exactly as you suggest (thanks). Originally I had been using the version downloaded from the main website (not sure if this has been updated since), which did not seem to format the datatype declarations so well.
Thanks, Matthew On 02/06/14 01:02, Michael Norrish wrote: > 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 -- Matthew Gadd <[email protected]> ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
