Avoid warning messages when loading realLib under Poly/ML.

Removed a bunch of rarely used functions from hol88Lib. Related documentation
updated.

The ancient hol88 interface should disappear eventually; code using it should
be properly ported to use the current HOL functions instead.

Change & (the overloaded injection function from natural numbers into
other numeric types), to be a prefix symbol in the grammar. This
allows things like -&n to pretty-print better. There are a few
breakages here and there. I realise that the type-annotation suffix
should be looser than &'s precedence level so that &n:int parses as
(&n):int rather than &(n:int). Changing this revealed some faults in
the handling of operators like unary minus, so the construction of the
precedence matrix in term_parse needed to change a little. Changes to
later files and theories were mainly caused by people writing ``&``;
you now need to write ``$&``, or ``(&)``.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Follow-on to the change to the pre-processor. There's a significant
problem, in that the heretofore standard way of protecting a
piece of code from alterations to the grammar(s) used to parse
terms in that piece of code ... no longer works after the change.

The previous recommendation was to re-bind Type and Term with

val (Type,Term) = Parse.parse_from_grammars <grms>

which allowed subsequent

Term ` .... `

to parse with the specified grammar. However, also

`` ... ``

would subsequently use the specified grammar as well. But I
changed the pre-processor, and this broke the usage of

`` ... ``

with the specified grammar.

The fix is to do as in src/real/RealArith.sml: get the
ambient grammar, set the desired grammar, execute the
body of code, then reset to the ambient grammar. Works
provided the code doesn't alter the grammar.

This probably needs to be documented in a more visible place,
once Michael comments.

Remove an unnecessary loading message, and add regression tests for
calculation over the real numbers. Discover a bug in the handling
of abs thereby. Fix to follow.

Revise the implementation of tracing so that term_to_string is only
called if a message is actually going to be emitted.

Remove more bad uses of term equality, and replace them with aconv.

The use of prove here meant that the behaviour of the code changed when
run from Holmake without the --qof flag attached. All the other uses
of prove in this file are fine because they are of things that are
supposed to be true: here the argument may or may not be true.

Some preliminary updates to this code, prior to a more extensive change
to make it handle fractions:
- some reformatting
- new entry-point tactic that pays attention to assumptions
- enable run-time choice of tracing

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

Changing arithLib to numLib. And RealSS to realSimps.

The reals library builds on Kan.0.

Minor changes to use "jrhUtils" instead of "useful".

Fixes in order to remove library file dependencies on global grammars.

Upgraded to use overloading.

Changes to accomodate new-look portableML. Also changes to term
nets mandate new (and improved) proofs of theorems in
hratScript, seqScript, and transcScript.

Note the usual culprits are rewriting with MULT_CLAUSES, ADD_CLAUSES,
and rewriting simultaneously with left and right distributivity.
People shouldn't do that!

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision