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

Added rich_topologyTheory and dependents

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

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.

----------------------------------------------------------------------

Edited the "real" library to use the new quotient library.

The hrealScript.sml and realScript.sml files only had a mention of
EquivType in a comment, not for actual use; these have been deleted.

The hratScript.sml and realaxScript.sml actually used the EquivType
tool to do quotients; this has now been revised to use the quotient
tool. In each case one new well-formedness (respectfulness) theorem
had to be proven and included as an argument to the tool.

In seqScript.sml, there was a small incompatibility where a definition
of a new constant named "-->" conflicted with the constant "--> defined
in the quotient library. This was healed by hiding the previous definition
before making the new one.

All of this was very straightforward.

Modified Files:
hol98/src/real/hratScript.sml hol98/src/real/hrealScript.sml
hol98/src/real/realScript.sml hol98/src/real/realaxScript.sml
hol98/src/real/seqScript.sml
----------------------------------------------------------------------

More useful theorems about reals and real-valued sequences.

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