Remove trailing whitespace.

Added an option to forcibly set the latex output of thms/terms/types. Slightly generalised formating options. Improved documentation.

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.

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

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.