Let help-system .doc files include Unicode ≤ and subtraction symbols

These need to be translated to LaTeX equivalents for the REFERENCE
manual.

Make Reference manual letter sections begin with correct entry

In particular, it previously began the sections with the first occurrence
of a lower-case letter; now it begins correctly with the first
occurrence, whether upper or lower case.

Also rename files corresponding to some symbolic identifiers to simply
have those names on disk too. Some characters (>, &) require
backslashes when typing these names in typical Unix shells, but as
long as we don't want to document /, we might as well use the
characters we're allowed to.

Let .doc files use ∃ and have LaTeX cope

Promote (SML) $ to Lib; update its fixity; document it

Added hyperlinks and sections (based on initial letters) in HOL REFERENCE

Support Unicode propositional connectives in .doc files

Support Unicode gamma (γ) in .doc files

Get TeX-translated doc files to handle more Unicode characters

Document add_strliteral_form in REFERENCE and DESCRIPTION

help: handle ⁻¹ (Unicode superscript -1) in .doc files

Make sure that “..” is handled in verbatim blocks as well as inline

Remove -- from doc-files.

Thanks to Andreas for pointing this out.

Allow for emphasis in .doc files by using *-delimiters

Adjust .doc processors to die with more information

In Poly/ML at least, you need to explicitly catch and do something with
exceptions. Otherwise, the process quietly dies with an error exit code.

Handle Docfile parsing exception better.

This is important because Poly's behaviour is to silently exit with a
success code (at least in generated executables).

Add a 'be verbose' flag to Doc2Tex.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Got the help build system working on PolyML.

Start working on porting the doc building system to SML (i.e., not Moscow ML)
to get it working with Poly ML.