It's true that the repository version has had some work done on this since the last release. I'm glad to hear that it's getting you nice results.
Michael > On 2 Jun 2014, at 20:11, "Matthew Gadd" <mg...@cam.ac.uk> wrote: > > 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 <mg...@cam.ac.uk> > ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ 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
