Fix many selftests to have prettier output

Delete trailing whitespace in src/

test of find_in, apropos_in, in src/bool/selftest

Add regression test for itself pretty-printing bug that Anthony found.

Add a slew of self-tests for term pretty-printer.

The last of these fails.

* coloured abstraction printing.
* coloured printing under a forall
* coloured printing let expression.
* coloured let printing when let-binding an abstraction.
* printing types on bound vars with show_types = true.
* test for variable-colouring in monad syntax.

Fix for TypeNet bug (and new regression test in src/bool).

The issue wasn't really anything to do with Hol_datatype. It was having
problems because of the way it inserts data about new types into the
TypeBase after a type has been defined. The TypeNet structure is used by
the type-abbreviation facility too, and so the 'same' bug can be
demonstrated using type_abbrev. The fix to TypeNet was to get it to
explicitly record the arity of the type operators in the nodes of its
internal trie.

Fix p/printing with show_types on to properly resolve polymorphic situations.

Include a test-case.

Fix another Unicode-bounce bug.

The real problem in the previous bug was that the Unicode flag was being
bounced as a term was printed for inclusion in the generated theory file.
The previous fix merely removed the bouncing. This fix deals with the
code around the bouncing properly, and simplifies the handling of Unicode
overloads.

Strange Unicode overload bug test-case.

New test illustrating minor problem in HO_MATCH_MP_TAC.

Fix pprint bug with Unicode binders in ProvideUnicode and add selftest.

Adjust a whole bunch of selftests to use Unicode at zero. In some
cases this is just for the sake of prettiness (making columns line
up), but in others, where the test is of the pretty-printer, I didn't
want to alter the tests.

Add a selftest to catch the soundness bug in the experimental kernel
that Peter Homeier discovered (and fixed).

Variables in the patterns of case expressions are now properly
'fresh'. They bind expressions on the other side of the case-arrow,
but do not affect variables outside the case expression or in other
branches. This revealed a bug in DecodeScript, where a theorem about
encoding sums ended up being about sums of type 'a + 'a only because
case pattern variables that should have been independent weren't.

Fix a bug in the pretty-printing of case expressions when they have
function type and are applied to argument(s).

Modify lexing so that "mixed" tokens are possible if a user puts them
into the grammar. For example, one might do

set_fixity "-->a" (Infix(NONASSOC, 450))

This then causes ``p -->a q`` to be parsed as an infix application of
-->a to p and q. If you wrote ``p --> a q``, the -->a token would not
be seen. Without -->a being in the grammar, it will be lexed as
before, a symbolic token (-->) followed by an alphanumeric one (a).
(Note also that things like --a--> where the mixing up happens in the
middle of the token, are just as possible.)

This change also allows traditional alphanumeric identifiers to
combine with Unicode subscripts. Using LaTeX notation, a_1 is now
possible.

The system builds with selftest level 1, so I believe I have preserved
backwards compatibility. (I have also added a test to
src/bool/selftest.sml to check for _1 working as a case expression
pattern properly.)

Handle merging of symbolic characters better when pretty-printing.

Find and correct a pretty-printing bug for let-expressions caused by
my recent implementation of syntactic patterns. There's another
similar bug in the handling of set comprehensions (next check-in).

Let expressions weren't printing correctly. Fix this problem and add
a regression test to catch it in future.

Test demonstrating a bug I'm about to fix in the Term parser.

Cleaning up more robustly when the program exits.

More regression testing for a bug that I am about to check in a fix for
(at least in the experimental kernel). When new_theory deleted any old
segment, the calls to Term.del_segment, and Type.del_segment did not
result in the appropriate calls to prim_delete_const and the Type equivalent
of this. This meant that old constant names did not get oldified, causing
a soundness bug.

Of course, it helps if the selftest compiles.

Self-test addition to catch the behaviour that allowed false to be proven.

A fix for the HOL Light INST_TYPE bug, that also affected the
experimental kernel. Basically, you can't blindly do type instantiation
across a theorem because it may cause what was a free variable to
become captured. The dB implementation is immune to this of course.
Test for the bug in the selftest program to extend the regression suite.

Added a very simple set of tests of substitution over terms. If we
should ever find a bug in the substitution code (heaven forbid!) it
can be recorded here to provide a regression suite.
Note that there are implicitly tests of aconv and the parser here as
well.