Fix TeX code to compile- some tests still not passing

Provide a compact datatype printing option for \HOLthm

With test-case and brief description in DESCRIPTION.

Closes #372

Fix many selftests to have prettier output

Const annotation in the pretty-printer wasn't happening for binders.

Fix a horrid bug in removing rules from grammars.

Sense of a test was inverted when working over a grammar's binders.

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

Make EmitTeX's printer do the right thing with type abbreviations

Fiddle with datatype printing in TeX (with selftest of sorts)

Adjust TeX selftest to cope with desired change in bd4bf27aabb209

Make constant annotations appear in more places when pretty-printing.

This affects the TeX selftests, which now see those \HOLConst
annotations (as desired).

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Add another EmitTeX UNIV pretty-printing test.

EmitTeX test failed under mosml because it ran in a ctxt w/out sets.

By putting open bossLib at the top of the file, we ensure that sets are
loaded. Under Poly/ML the selftest was running with the full hol
image, which implicitly gives you a context where bossLib is already
loaded.

Test a couple of instances of UNIV-printing in TeX.

These pass thanks to 45d91cfc013ef.

Modify EmitTeX to allow for 'dollarised' printing without parens.

This means that an infix symbol can be printed without any decoration at
all, which might be useful. Default behaviour, as before, is to use
parentheses to protect the bare sugar-symbols.

Modify printing of $if test to reflect insertion of HOLKeyword macro.

A couple of (failing) tests of the munger's printing of dollared syntax.

Tidy up src/Tex's selftest.

Some selftests for EmitTeX, particularly overrides

The tests on constants and tokens fail with the recent changes to
pretty-printing. However, they succeed in revision 8827.
I'm mostly sure they adhere to the intended semantics of overrides.