Fix quotient/examples/{lambda,sigma} given tight equality

Remove -- as an alias for Term parser.

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

Clean quotient examples: now use core Mutual lib, rather than own copy

This is a start, of sorts, on having a go at github issue #10

Found that these quotient examples do not work right in Poly/ML; although they build, they cannot load. The reason is that in Poly/ML, one cannot say

val NAME = ...

if NAME has been previously defined as an ML constructor. In this case, a theorem was being saved named "DIFF", and DIFF is a constructor defined in Lib.sml:

datatype 'a delta = SAME | DIFF of 'a

The "val DIFF = ..." was fine in MoscowML, not even a warning, but is an unrecoverable error in Poly/ML.

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 revised versions of the quotient examples. The change from
(. => . | .) to (if . then . else .) caused the old versions to break.

Modified Files:
lambda/alphaScript.sml lambda/termScript.sml
lambda/variableScript.sml sigma/alphaScript.sml
sigma/objectScript.sml sigma/variableScript.sml
----------------------------------------------------------------------

----------------------------------------------------------------------
Committing in a new example for the higher order quotient library.
This represents the abstract syntax of the lambda calculus, with
alpha-equivalent terms identified.

Modified Files:
README
Added Files:
lambda/MutualIndThen.sig lambda/MutualIndThen.sml
lambda/alphaScript.sml lambda/barendregt.sig
lambda/barendregt.sml lambda/betaScript.sml
lambda/etaScript.sml lambda/ind_rel.sig lambda/ind_rel.sml
lambda/liftScript.sml lambda/more_listScript.sml
lambda/more_setScript.sml lambda/reductionScript.sml
lambda/tactics.sig lambda/tactics.sml lambda/termScript.sml
lambda/variableScript.sml
----------------------------------------------------------------------