#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
3b438179 |
|
04-May-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Added an option to forcibly set the latex output of thms/terms/types. Slightly generalised formating options. Improved documentation.
|
#
135ee45e |
|
29-Apr-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Better error reporting and hopefully fixes the problem building under mosml reported by Michael.
|
#
840364ee |
|
28-Apr-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Minimize the memory Latex needs, by removing definitions of terms that never get printed and moving the index in an input file instead of a macro. In combination with an extension of the hdf-file-format this allows printing of whole (large) theories in indices now.
|
#
1d441253 |
|
20-Apr-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some more updates and extensions of holindex. In particular: - sorting the index by occurence - adding comments to the index - allow arbitrary keys for theorems and with that multiple instances of the same theorem - fine control which theorems / terms / types are printed in the index See holindex-demo.tex for more explanations
|
#
ee821925 |
|
18-Apr-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make holindexData.sml use a signature in order to get it to compile with mosml.
|
#
74a2ef8e |
|
18-Apr-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Addition of a tool called "holindex". Holindex is an extension of the munger. It uses the munger to create Indexes of HOL Theorems, Terms and Types in latex documents. However, it can also be used to add just some HOL terms/types/theorems in the text. In contrast to the munger which preprocesses inputs before handing them to latex, holindex uses auxiliary files similar to what bibtex or makeindex do. The first run of latex on "something.tex" will create a file "something.hix" (hol index). A call of "munge -index something" will create then a file "something.tix" (latex index) that is used for the next runs of latex. Similar to the munger, theorems are loaded from the libraries. However, terms and types can be stored in a special auxiliary files with the ending ".hdf" (hol definitions). Please see holindex-demo.tex for an example.
|