Provide >>~ option to munging commands

This version of indentation provides another way to attack the problem
of getting nice indentation under turnstiles. For example,

\vdash\;\HOLthm[>>~4,nostile]{thy.thm}

seems to do a good job when using \; as one's math-mode spacing and
with font = 11pt Computer Modern. As per the Description text, other
effects are also possible.

Correct some TeX-munging bugs to do with >> option

Fix TeX code to compile- some tests still not passing

Get TeX/mungeTools to build again

make \HOLty[of] respect instantiation options

so, for example, \HOLty[of,:'b/:'a]{MAP} will print a specialised type
for MAP on a 'b->'b function rather than the general 'a->'b version,
without requiring the user to type the full instantiated type as an
annotation.

Making parsing of trace-setting munger option a bit more robust

Set arbitrary traces while LaTeX munging.

Closes #141. That issue calls for a slightly different interface to
get much the same effect. This approach has the advantage that it
keeps the effect of the trace changing localised.

Implement, document new form of substitution for LaTeX munging

Implement nomath option to munger commands to override global -m option.

make the munger overload removal option work for types too

in which case it disables type abbreviations for that name

add an option to the munger for controlling the print depth

add rulename option to LaTeX munger for naming inference rules

Allows the user to provide a string (name) to be passed as the optional
argument to \infer[name]{...} when typesetting using rule or
stackedrule.

Due to the simplistic parsing of the munger's commands and options,
unexpected results are likely if this name contains any special
characters. (Perhaps it should parse them under some encoding for this
option?) The name is wrapped in a new \HOLRuleName command, which
provides a route for customisation.

munger: allow showtypes to take an argument indicating the trace level

Looking at the output of setting the types trace to 2, this is probably
fairly useless. But it's backwards compatible and (hopefully) benign.

User can specify strings not be overloaded when a term is printed

The syntax is something like

\HOLtm[-mystring1,-mystring2]{mystring1 mystring2}

This is useful when explaining notation.

Remove a compile-time warning due to non-exhaustive matching

Fix munger bug where math-mode option conflicted with var-substitutions

In particular, something like

\HOLthm[m/x]{theorem-name}

was parsed as an attempt to set the math-mode spacing to /x instead of
as a substitution of name m for name x.

Improve TeX-mungers' usage messages.

Preliminary thoughts towards allowing math-mode spacing in HOL TeX.

Allow type instantiation to be performed on arguments to \HOLtm and \HOLthm.

EmitTeX: new merge and nomerge options to \HOLtm and \HOLthm.

These allow per-entity control of whether or not token-merging analysis is
done. For example, with it globally off (using --nomergeanalysis), theorems
involving LEAST will print with the bound variable squished up against the
LEAST: ... (LEASTn. P n).

Putting merge back on for this one theorem will get the nice spacing
back again.

EmitTex: do variable-renaming instantiation after SPEC_ALL, not before.

This lets something like [m/n,n/m] work on theorems like |- !m n. foo m n
when those theorems have SPEC_ALL applied to them (as is the default).
The code that attempts to do renaming of bound variables has no way to
achieve the required simultaneity so will introduce unwanted priming if
[m/n,n/m] is applied to bound variables.

Add new --nomergeanalysis option to mungers (documented in Description).

Implement & document nodollarparens option for the TeX munger.

Fix bug in latest commit to do with unhandled UNCHANGED exceptions.

Make instantiations in munger change all vars, free or bound.

Add 'stackedrule' option for stacking rule hypotheses.

Add 'rule' option for implications (in terms or theorems).

Requires the proof package for its \infer command.

Provide another level of indirection for HOL inline stuff.

New LaTeX command, \HOLinline{....}.

New 'conj' option for munging theorems (accesses individual conjuncts).

Add new spaceddef option to put blank lines between definition conjuncts.

Added a trace to EmitTeX for printing datatype theorems with the name of the type before the equals sign (instead of a variable).

The old behavior is still default, because scripts for emitting SML that use datatype_thm_to_string would want the bare variable before the = sign. However, the new behavior looks better in TeX, so I turn the trace on in the munger.

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.

Allow >> option to be followed by digits to specify different indent level.

Also extend the implementation to affect \HOLty, and document it in the
DESCRIPTION.

Get >> to work with \HOLthm; removing automatic indenting with def option.

Flip order of application of turnstile and indent options in term-printing.

Add a showtypes option to the munger, for printing terms and theorems.

munger: fix error message when an instantiation fails.

munger: make tt mode default for terms, types; add alltt option to flip back.

Allow blank lines in overrides files passed as c/line parameters to mungers.

Allow width to be specified on a per-instance basis with a width=x option.

Allow commandline to specify the linewidth used by munger when p/printing.

Modify mungeTools so that Moscow ML can compile it.

Start of implementation of LaTeX munging for HOL.

Work based on a tool developed by Ramana Kumar.