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.