Remove TABs from src

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

Foolishly missed a QCONV. Picked thanks to a Cholera (un-)build.

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

A dramatic efficiency improvement for this code (particularly in conjunction
with the recent change to Term.subst).

More efficient version of this. This function still dominates in the
running time of UNWIND_EXISTS_CONV, which is, of course, totally
ridiculous, and further proof that deBruijn indices must go! Ahem.

Pulled LAST_FORALL_CONV out of src/simp/src/Unwind.sml to join its sibling
LAST_EXISTS_CONV in the "standard" collection of conversions.

Fixes for bugs caused by using direct equality on terms. Exploits for these
require creation of terms that have explicit substitutions in just the
right places, but shouldn't be too hard to imagine. Also added
term_eq to the Term signature to be a safe curried equality.

Paired syntax.

liteLib's definition of is_imp and dest_imp must come before boolLib's
because we want the HOL88 behaviour, not the rational HOL Light behaviour.

Fix a bug caused by fact that Ho_Rewrite no longer exports REWR_CONV, but
that this function is now Conv.HO_REWR_CONV.

Slight improvement to comments.

Updated UNWIND_FORALL_CONV to cope with a wider range of bodies. In
particular it now copes with things like !x. ~(x = e) \/ ....

Why roll your own propositional d.p. when Richard wrote one yonks ago?
My last attempt didn't cope with ~p as the last conclusion of a term,
and I couldn't be bothered fixing it. tautLib moves earlier in the
build sequence as a result.

Change aiming to fix a bug whereby UNWIND_FORALL_CONV couldn't
handle
!x. (P x ==> Q x ==> (x = e)) /\ (x = e) ==> R x
Also removes use of prove.

Elimination of dependence on Ho_theorems.

As is so often the way, the fix introduced a worse bug. Hrumph.
Anyway, it's fixed now.

Fix to a long-standing bug bound up with higher-order matching.
Viz:
- SIMP_CONV bool_ss [] (--`?y x. P y /\ Q x /\ (y = f)`--);
<<HOL message: inventing new type variable names: 'a, 'b.>>
> val it =
|- (?y x. P y /\ Q x /\ (y = f)) = ?y x. P y /\ Q x /\ (y = f)
: Thm.thm
Unwinding (as implemented in Unwind.sml) should take care of the equality
with y, but doesn't. But now this is fixed.

Fixes in order to remove library file dependencies on global grammars.

Upgraded to use overloading.

Initial revision