For some reason I cannot build acmart-based articles when makeidx is loaded

Product measure and Tonelli's theorem

Updated HOL Description for mathematical theories (with other cumulative fixes)

TeX-munging: Fix HOLStringLit{SG,DG} macros

Thanks to Yong Kiam Tan for catching the errors.

Fix TeX-munging for extended string literals

Uses new TeX macros (which can be redefined if desired).

Make definitions use a different equality symbol

By default the symbol is an equality with a "def" written on top of
it, but this can be changed with a renewcommand of
\HOLTokenDefEquality.

Documented in DESCRIPTION, tested in src/TeX/theory_tests.

Added TeX notation for relation inversion (relinv)

Added TeX_notation for "++" in listTheory

Added TeX notation for O (relation composition)

TeX notations for RUNION, RINTER and RSUBSET in relationTheory

Pretty-printer now annotates consts with their real names and types.

In "complicated" overload situations, such as the overloads for NOTIN
and <>, the annotation can't point to a "real" underlying constant,
but does still provide the type for the emacs tool-tips.

In passing, also create a new annotation form, the SymConst as well as
the Const. This is done for the TeX backend's benefit, so that it can
avoid treating things like + the same as normal identifiers. This
works well for math-mode munging where you want "+" to map to $+$, but
want "INSERT" to map to \textsf{INSERT}.

Closes #39

Finish documenting math-mode munging.

Closes #121.

translate tildes in EmitTeX strings

Made an new HOLTokenTilde command as the target. The default behaviour
of that command might be improved, but I don't know how (typesetting a
tilde nicely in TeX is apparently pretty hard...).

Handle character literals when printing to LaTeX

Closes #190.

See also 89b5d3224403 for first piece of work in this vein.

Define \HOLFieldName macro rather than \HOLFldName

Bug spotted by Ramana.

Create new PP backend annotations for literals (strings, numbers, ...)

Use these to emit string literals via a \HOLStringLit macro that can
be redefined to get better output than my default. Of course, it's
quite possible that my \textrm{``#1''} is not even a reasonable
default.

Note how the HOLStringLit macro is given an argument that doesn't have
the quotation mark delimiters around it.

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.

Provide for special typesetting of type-operators in EmitTeX.

This uses back-end annotations.

Use Const annotations in the TeX pretty-printing backend.

Intention is to allow users to redefine \HOLConst to set their
constant names in something other than the default \texttt.

Make EmitTeX always use a tt double-quote (around strings).

Give isPREFIX symbols TeX equivalents.

Allow empty list forms to be overloaded ([], {}, etc).

This gives us the ability to get nice TeX for them. Instantiate this ability
for emptyset.

Merging \inlineHOL in holindex.sty with Michael's newly added \HOLinline in
holtexbasic.sty. To keep things consistent "blockHOL" has been renamed to
"HOLblock" and moved to holtexbasic.sty.

Provide another level of indirection for HOL inline stuff.

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

First attempt at TeX notation for lazy list brackets.

Add TeX notation for 'proper subset'.

Add TeX notation for bag delimiters.

Fix leaching of boldness from HOLKeyword command by adding braces.

Add TeX notations for some HOL keywords: if-then-else, case-of, let-and-in and
do-od.

Added HOLTokenDot to holtexbasic.sty

Give a TeX binding for Hilbert choice, now generated in TeX from @.

Add support for super- and sub-scripts in the LaTeX backend of EmitTeX.

Fix errors in last EmitTeX check-in. Handle superscript -1 in overrides.

More unicode symbols for EmitTeX's string_map. Also added new HOLTokens for rhd, left and right small triangles, and composition (circ).

More symbols for EmitTeX (subset and submap).

Use annotation information to italicise variables in EmitTeX.

This can be customised through LaTeX redefinition of the commands
\HOLFreeVar and \HOLBoundVar. Both current make their arguments
\mathit.

Add union and intersection to EmitTeX's known symbols.

Add superscript star and plus to EmitTeX.
Generalisation opportunities probably exist.

Added new (Unicode) symbols to EmitTeX

holtexbasic.sty: \notin looks slightly better than \not\in.

Improve printing of HOL data types -- now more compact.

Extended the filtering to eliminate big record definitions.

Added LaTeX tokens for IN (\in) and NOTIN (\not\in).

Update to EmitTeX, following changes to pretty-printing in HOL.

Add a leftarrow token.

Moving TeX.