Remove TABs from src

Will also make selftest to check that they aren't introduced

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

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

Generalise and correct "weak congruence" handling.

Some notes:
- Add extra tracing, including to congruence rule application in
simplifier.

In particular, spit out a message when a hypothesis is recognised as
a side condition rather than something that will prompt a recursive
invocation of the 'depther'.

- If rewriting with a relation that includes a variable that gets
instantiated, the specific relation being used needs to be included
in the argument that gets passed to the reducer. How else is the
atomic rewriting step to know which theorem is to be produced?
Think of rewriting MOD 5, say. When it happens upon argument 7, the
atomic step should produce MODEQ 5 7 (7 MOD 5), where MODEQ 5 is the
rewriting relation.

- Congruence opener needs to avoid treating user vars as genvars.

Hitherto, it was looking at the RHS of the congruence's conclusion
and treating all the vars there as things that were due to get
instantiated through the recursive invocation of the simplifier.
But if the relation can take a variable, that variable may come from
the conclusion.

In particular, imagine

0 < n ==> MODEQ n genv1 genv2 ==> (genv1 MOD n = genv2 MOD n)

The n has been instantiated from the term to be rewritten, and
shouldn't be viewed as a genvar.

Generalise congruence API to handle terms with free vars as equivs.

Remove a couple of non-exhaustive pattern-bindings in liteLib and simp/Opening.

This reduces poly compilation output clutter.

Fix an error in the simplifier's tracing of congruence rule
application; when it rewrites a congruence assumption, it said the
conclusion rather than the assumption was rewritten.

Fully support weaker relations than equality that aren't also
constants. Start to implement a reduction engine for beta-reduction
in the lambda-calculus. Still some wrinkles to work out.

Change relations that have congruence rules stored for them
(they have to be preorders) to be stored as terms rather than string
pairs (the latter encoded theory and term name, allowing constants
only). The samerel function is now what should be used to determine
if two preorders are compatible. The use of same_const and aconv
means that only single constants can be used polymorphically, but
arbitrary monomorphic terms can be used elsewhere. (It's possible
this breaks Thomas Türk's examples; I have run selftest 1 on
everything else.)

Changed CONGPROC to be able to handle congruences that use more than one congruence relation. Now the original function producing reflexivity theorems for the used congruence relation is given an extra argument to decide for which congruence to produce a reflexivity theorem. Otherwise CONGPROC did not needed to be adapted.

A fix for a bug in the simplifier's treatment of congruence rules that
prevented it from handling "higher order" rules, like this one for
RES_FORALL:

|- (P = Q) ==> (!x. x IN P ==> (f x = g x)) ==>
(RES_FORALL P f = RES_FORALL Q g)

Feeling brave, I then put this, and the accompanying rule for RES_EXISTS
into bool_ss. Congruence rules take precedence over normal term traversal
in the simplifier, so with a rule like the above installed, the constant
RES_FORALL is never "seen" on its own. In particular, this means that
you can't rewrite with RES_FORALL_DEF, which looks like

|- RES_FORALL = (\p m. !x. x IN p ==> m x)

Instead, you need to rewrite with something that matches at the same level
(or higher) as the congruence rule. Thus, RES_{FORALL,EXISTS,SELECT}_THM
in boolTheory. These can then be the basis for the theorems in
res_quanScript, and look like

|- RES_FORALL P f = !x. x IN P ==> f x

Two significant changes here:
1. make the code more forgiving about the form of congruence rules;
it was fussy primarily so that it could spot congruence rules
accurately over relations other than equality. These are
impossible to use at the moment, and when the relation is
equality, it's useful to have more fexibility.
For example, an applicative order evaluation rule for LET:
(v = v') ==> (LET f v = f v')
would have been disallowed under the old rules because the left-hand
side and the rhs were not substitution instances of each other.
2. fix a bug causing terms mentioning variables used in a congruence
to fail to be rewritten. Try,
SIMP_CONV bool_ss [] ``p /\ x' ==> x' /\ y``
the congruence for implications won't fire, and the second x'
won't get written away, all because the implication congruence
rule has x' as one of its variables. GSPEC o GEN_ALL brings
genvars to the rescue.

Fix to remove an exponential blow-up when traversing a term with
congruence rules. The problem is that when traversal with congruence rule
1 fails to change the term, traversal with the next rule is attempted.
But, when looking at a sub-term within the second traversal, both
congruence procedures will be tried once more. You can see the badness
with

- set_trace "simplifier" 2;
- SIMP_CONV bool_ss [] ``p ==> q ==> r``

You will see the line

more context: [.] |- q

twice. This problem is hard to notice in normal contexts because the only
built-in congruence rules are for implication and conditionals, and these
are not usually nested very deep. However, big conjunctions and a rule for
conjunction combine to produce very bad performance. Till now anyway!

Now, congruence procedures that "work", but which do not change the term,
mask other congruence procedures.

Fairly radical changes: theorems' hypotheses now stored in a binary tree.

Paired syntax.

Elimination of dependence on Ho_theorems.

Initial revision