Moved abstract topology stuff outside of "src/real", remaining stuff is metricTheory now.

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Fix real theories in light of pat_assum rename

Add definition of rpow function, contributed by Umair Siddique.

This is exponentiation where both arguments are real numbers. Hitherto,
realTheory has only had pow, where the exponent had to be a natural
number.

Document this in release notes.

Remove unnecessary infix declaration in transcScript.sml

Removed further functions from hol88Lib.

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 ``(&)``.

Did some community service expunging all occurrences of the old syntax for
if-then-else from the HOL distribution.

Apologies if I've broken your example or development: you can either upgrade
it to use the new syntax or else issue the magic parser incantation that
I chopped out of boolScript.sml on this check in.

Collection of minor alterations.

Hiding the "B" constant, except if realLib is loaded ... that seems
to be a mistake, now that I think about it.

Tracking move of Num_induct to numLib.

The reals library builds on Kan.0.

Changes due to the incorporation of John Harrison's datatype definition
package.
Many of these due to the fact that `n:num + b` parses differently because
sumTheory is now in the ancestry. A couple of other changes due to
explicit references one or two proofs made to num_Axiom. These are now
to num_Axiom_old.

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

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