Fix pretty-printing of real and relation inverses

Now both get to keep their pretty superscript forms (-1 for the reals,
and T for the relations) even when both theories are loaded. The cost
is that neither will be printed as "inv" when unapplied to arguments,
instead appearing as "realinv" and "relinv" respectively.

Closes #481

Remove -- as an alias for Term parser.

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

Add rule for "inv" in realaxTheory.

Previously the superscript T rule from relationTheory was active.

Remove unnecessary structure bracketting

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

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Removed further functions from hol88Lib.

Implement unary minus (the old ~ still also works). Selftest level 2
passes. Changes in the "words world" were replacing $- with -. In
the two quotient changes, I made sure that the infix operator
that used the - character was part of the grammar before it was
parsed. This is necessary because - is now a non-aggregating
character, mainly so that ``--p`` parses as three tokens, not two. Of
course, if you added -- to your grammar, then it would go back to
parsing as two.

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

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.

----------------------------------------------------------------------
Enter Log. Lines beginning with `CVS:' are removed automatically

Committing in a revision to the quotients library, with associated
corrections to the dependent libraries.

Added a feature requested by Michael Norrish, that the tool generate
trivial respectfulness theorems if the user leaves them out, of the
form
!x y. (x = y) ==> (treal_of_hreal x) treal_eq (treal_of_hreal y)

where the relation is a true equivalence relation, i.e., reflexive.

This enabled the deletion of three trivial respectfulness theorems
that I had added when moving the dependent libraries to use the new
quotient tool. Harrison's tool had not required these, because his
system only dealt with true equivalence relations, which are always
reflexive, so in the above example, the respectfulness of treal_of_hreal
was easy to prove.

Also added a feature to check that all of the constants being lifted
are properly represented by respectfulness theorems. This is only
sensible, and should catch a simple and common user error.

Also divided the quotientScript.sml file into five, adding four
new files for the four type operators "list", "option", "pair", and
"sum". Each has the definitions and theorems appropriate for that
type operator, and for some of the common constants associated with
the type operator.

Also added quotientLib.sml, which includes all the others. Thus a
user can easily get everything in the quotient library by simply
typing "open quotientLib;".

Modified Files:
hol98/src/integer/integerScript.sml
hol98/src/n_bit/wordFunctor.sml
hol98/src/quotient/src/quotient.sig
hol98/src/quotient/src/quotient.sml
hol98/src/quotient/src/quotientScript.sml
hol98/src/real/hratScript.sml hol98/src/real/realaxScript.sml
Added Files:
hol98/src/quotient/src/quotientLib.sml
hol98/src/quotient/src/quotient_listScript.sml
hol98/src/quotient/src/quotient_optionScript.sml
hol98/src/quotient/src/quotient_pairScript.sml
hol98/src/quotient/src/quotient_sumScript.sml
----------------------------------------------------------------------

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

Committing in src/real/realaxScript.sml.

I left a small extra "handle e => Raise e" in the file, which is
not needed. This update just cleans that out.

Modified Files:
hol98/src/real/realaxScript.sml
----------------------------------------------------------------------

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

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

Bad uses of term equalities.

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.

Fix to make it build now that = is non-associative.

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

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