Get quotient/examples to build given tight equality

Remove -- as an alias for Term parser.

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

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.

Revision 8066 caused the msgScript.sml example of the quotients package to break. This revision repairs the example.

msgScript.sml used "U" as a variable inside of theorems, e.g.

freenonces_RSP:
|- !U V. msgrel U V ==> (freenonces1 U = freenonces1 V)

but revision 8066 now reserves U as a specially parsed form, to represent UNIV.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

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

Committing in two new examples of using the quotient package.

The first is a very simple example, duplicating Paulson' most complex
example from his quotients paper.

The other is the most complex example so far, creating the syntax of
Abadi and Cardelli's sigma calculus, and proving the Church-Rosser
theorem for this language. The quotient package is used in the file
"liftScript.sml". This is the example from the 45-page paper in the
"doc" subdirectory.

To build either of these go to the directory where the example is
located and type Holmake.

Modified Files:
hol98/src/quotient/src/quotient.sml
Added Files:
hol98/src/quotient/examples/msgScript.sml
hol98/src/quotient/examples/obj/MutualIndThen.sig
hol98/src/quotient/examples/obj/MutualIndThen.sml
hol98/src/quotient/examples/obj/alphaScript.sml
hol98/src/quotient/examples/obj/barendregt.sig
hol98/src/quotient/examples/obj/barendregt.sml
hol98/src/quotient/examples/obj/ind_rel.sig
hol98/src/quotient/examples/obj/ind_rel.sml
hol98/src/quotient/examples/obj/liftScript.sml
hol98/src/quotient/examples/obj/more_listScript.sml
hol98/src/quotient/examples/obj/more_setScript.sml
hol98/src/quotient/examples/obj/objectScript.sml
hol98/src/quotient/examples/obj/reductionScript.sml
hol98/src/quotient/examples/obj/semanticsScript.sml
hol98/src/quotient/examples/obj/tactics.sig
hol98/src/quotient/examples/obj/tactics.sml
hol98/src/quotient/examples/obj/variableScript.sml
----------------------------------------------------------------------