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.

Preserve add_user_printer properly in grammar data

This requires a slightly involved process for storing references to
code in theory files.

Update the .doc file on add_user_printer (which was already incredibly
long), and add a test.

Closes #367

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

Remove some duplicates of the theorem TRUTH.

These are:
• INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings)
• IN_APP_applied and IN_ABS_applied (inadvertently generated)

Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT).

These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").

Provide support for evaluating float to int and real to int operations.

For example, the following weren't working before (with intLib and realLib loaded):

EVAL ``NUM_FLOOR (-0.5)``; (* |- flr (-0.5) = 0 *)
EVAL ``NUM_CEILING 0.5``; (* |- clg 0.5 = 1 *)
EVAL ``INT_FLOOR 0.5``; (* |- flr 0.5 = 0 *)
EVAL ``INT_CEILING 0.5``; (* |- clg 0.5 = 1 *)

Improvements to evaluation coverage for realTheory.

Previously, the follow terms were failing to evaluate:

``sum (1, 4) real_of_num``
``1 > 1 / 2``
``1 >= 1 / 2``
``flr (232 / 3)``

The operation "sum" is now introduced using Define.

Give the real numbers decimal fractions.

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

INFINITE is now an abbreviation for ``\s. ~FINITE s``.

Prove some results about the finite-ness or otherwise of some universal sets.

Removed further functions from hol88Lib.

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Additional functionality for abbreviations.

1. The labels library has been merged into
markerLib and the src/labels directory eliminated.
2. Have added markerSyntax structure.
3. Operations on abbrevs used to all be in
structure Q, even those that didn't deal
with quotations (like UNABBREV_ALL_TAC). Now
markerLib provides all abbrev. operations and
these take terms. Operations that benefit from
quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc.
are still to be found in Q.
4. Abbrevs are kept reduced by the simplifiers and
there is a REABBREV_TAC which can be separately called.
This sorts abbrevs topologically, so that they get
restored in a sensible order.
5. For situations where one wants to get rid of all
abbrevs, apply a tactic, and then restore the abbrevs,
there is WITHOUT_ABBREVS: tactic->tactic.
6. Have added a simple topological sort to Lib.
7. Updated proofs in the src directories, and also
in examples/lambda.

Fix a silly hole in the automatic simplification of real number arithmetic.

Fix a number of calculation bugs, mostly calculations involving zero.
The new tests all used to fail.

Add more aggressive normalisation of multiplicative expressions to ARITH_ss.
Also provide old_arith_ss values for scripts that don't want this new
behaviour. Update proofs to go through again. Some should be a bit more
robust in the face of future changes to arith_ss. Others just punt and refer
to old_arith_ss.

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

Added floor and ceiling operations (mostly from Michael's NETSEM
stuff).

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

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
----------------------------------------------------------------------

Changed NUMERAL_BIT1 and NUMERAL_BIT2 to BIT1 and BIT2, respectively.
Sorry, they were just too long. Also, ALT_ZERO is now named ZERO.

Upgrades to ML code generation. It now works for numerals, although
the results of a computation will be incomprehensible usually. Writing
a prettyprinter needs to be done.

Handle exponentiation in the "real reduction" functionality. Done through
one big rewrite theorem (pow_rat) proved in realScript.sml.

Put this back the way it was.

Hmm. Not sure what this is.

First cut at calculation with the reals. Doesn't include a treatment of
exponentiation, nor does it eliminate divisors in fractions. Updates
stateful rewriter and global compset, so that EVAL will do calculations
with fractions.
Am about to go home with build just in the middle of probability. If
I've broken anything, apologies! Fix the bug by commenting out
++ REAL_REDUCE_ss
in the definition of real_ss in realSimps.sml

Little more progress with this stuff.

Moving towards calculation with the reals.

Added a lot of rewrite exports. Am tempted to add versions of store_thm
and save_thm to BasicProvers that do this exporting automatically.
I could call them "Store_thm" and "Save_thm", say. Please write if you
think this is a revolting idea. I'm not entirely convinced myself.

A few extra theorems to help with calculating with rational numbers.

Some more useful theorems about sup and inf.

A really useful theorem about supremums: for any 0 < e, you can
always gets within e of the supremum.

More theorems, this time about sup and inf.

More useful theorems about reals and real-valued sequences.

More real simplifications, and more theorems about pos, max and min.

As predicted, I need a few more simplifying rewrites.

Finally got around to fleshing out the real simpset (the other changes are
the ramifications of this!)

Major changes:

1. Got rid of AC rewrites for + and *. If you want them (perhaps for
compatibility with the old real_ss), use real_ac_ss.

2. Added a huge bunch of useful rewrites to real_ss, though I'm sure
I'll need to add a huge bunch more before I'm finished with it.

Some additions from HOL Light, in order to have proper basis for the
irrationality of root 2 proof.

Added new facilities for dropping or preferring certain numeric types
all at once. Documented one of the new functions, and fixed the
documentation for add_numeral_form, which now automatically adds the
appropriate overloading for "&" (I realised that we didn't need to
force the user to do this themselves).

Changed the way overloading handles numerals slightly so that &x will
now always be resolved as a function away from :num. (Whether it be from
:int or :real.) The drawback is that people need to explicitly overload
& if they develop a new numeric type.

Removed gratuitous incompatibility with Taupo-6 in type of set_fixity;
its type is now string -> fixity -> unit, rather than
(string * fixity) -> unit.

Changing arithLib to numLib. And RealSS to realSimps.

The reals library builds on Kan.0.

The function allow_for_overloading_on has been completely removed from
the system. The overload code now uses anti-unification of types to
figure out the least generalisation of all the types that an overloaded
operator needs to represent.

Minor changes.

In polyScript, the polynomial operators have been overloaded. We are
not sure whether this is a good idea or not.

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".

Removed a stray right parenthesis that the old parser hadn't been catching
as an error.

Upgraded to use overloading.

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

Initial revision