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.

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.

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

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

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

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

Tracking move of Num_induct to numLib.

The reals library builds on Kan.0.

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

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