Fix src/quotient/src/ for tightequality

Remove -- as an alias for Term parser.

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

trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

Ensure that seq$--> and quotient$--> have the same precedence.

Move more TeX-notations out of EmitTeX and into their 'home' theories.

Next step will be to completely remove the remaining entries in EmitTeX's
string_map.

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

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

Committing in fix to SRW_TAC so that it can solve elementary case
expressions, such as (case 1w of 1w -> x || _ -> y) = x.
Bug discovered by Anthony Fox.

Also commiting in extensions to quotient library to better support
the new constant 'literal_case'.

Modified Files:
hol98/src/HolCheck/stringBinTree.sml
hol98/src/basicProof/BasicProvers.sml
hol98/src/quotient/src/quotient.sml
hol98/src/quotient/src/quotientScript.sml
hol98/src/simp/src/boolSimps.sig
hol98/src/simp/src/boolSimps.sml
----------------------------------------------------------------------

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

Committing in slight fixes to the files that avoid some undetermined
types in theorems being proven.

Modified Files:
src/quotientScript.sml src/quotient_listScript.sml
src/quotient_optionScript.sml src/quotient_pairScript.sml
src/quotient_sumScript.sml
----------------------------------------------------------------------

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

Committing in modifications to the quotient library, to better support
lifting of theorems with mention of set operators, including INSERT,
SUBSET, FINITE, which may be applied to sets of types being lifted.
The previous version was very untested.
This is still experimental, but a great improvement.

Modified Files:
src/quotient.sml src/quotientScript.sml
src/quotient_pred_setScript.sml
----------------------------------------------------------------------

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

Committing in a revised version of the quotients package, where now
erroneous input theorems are usually detected early, and the erroneous
theorem listed in an error message. This should greatly improve the
usability of the package, especially for new users. Thanks to Michael
Norrish for prodding me on this one.

Also added a new version of finite sets from lists, due to Michael Norrish.

Also moved the "obj" directory to now be called "sigma"; this contains
the sigma calculus example from Abadi and Cardelli, as described in the
longer 45-page paper.

Modified Files:
hol98/src/quotient/examples/finite_setScript.sml
hol98/src/quotient/src/quotient.sml
hol98/src/quotient/src/quotientScript.sml
Added Files:
hol98/src/quotient/examples/ext_finite_setScript.sml
hol98/src/quotient/examples/sigma/MutualIndThen.sig
hol98/src/quotient/examples/sigma/MutualIndThen.sml
hol98/src/quotient/examples/sigma/alphaScript.sml
hol98/src/quotient/examples/sigma/barendregt.sig
hol98/src/quotient/examples/sigma/barendregt.sml
hol98/src/quotient/examples/sigma/ind_rel.sig
hol98/src/quotient/examples/sigma/ind_rel.sml
hol98/src/quotient/examples/sigma/liftScript.sml
hol98/src/quotient/examples/sigma/more_listScript.sml
hol98/src/quotient/examples/sigma/more_setScript.sml
hol98/src/quotient/examples/sigma/objectScript.sml
hol98/src/quotient/examples/sigma/reductionScript.sml
hol98/src/quotient/examples/sigma/semanticsScript.sml
hol98/src/quotient/examples/sigma/tactics.sig
hol98/src/quotient/examples/sigma/tactics.sml
hol98/src/quotient/examples/sigma/variableScript.sml
Removed Files:
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
----------------------------------------------------------------------

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

Committing in a revised version of the quotients package, and an example.

The quotient theorems are broken into theories based on the type operator
they refer to, with general non-specific theorems remaining in
quotientScript.sml.

The example of creating finite sets from lists by a quotient is presented
in the new "examples" directory, in finite_setScript.sml. It is perhaps
surprisingly simple to walk through.

Modified Files:
hol98/src/quotient/src/quotient.sml
hol98/src/quotient/src/quotientLib.sml
hol98/src/quotient/src/quotientScript.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
Added Files:
hol98/src/quotient/examples/finite_setScript.sml
hol98/src/quotient/examples/ind_rel.sig
hol98/src/quotient/examples/ind_rel.sml
hol98/src/quotient/src/quotient_pred_setScript.sml
----------------------------------------------------------------------

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

Remove fixity setting command for ++ so that ++ now sits at the "standard"
HOL position. This means that ++ is now left associative, and at a slightly
different precedence.

----------------------------------------------------------------------
Committing in the quotient library, including documentation.
These files were not properly added before.
Added Files:
hol98/src/quotient/doc/quotient2.pdf
hol98/src/quotient/doc/quotient2.ps
hol98/src/quotient/src/quotient.sig
hol98/src/quotient/src/quotient.sml
hol98/src/quotient/src/quotientScript.sml
----------------------------------------------------------------------