Remove eqtype declaration for term type

Removed ancient documentation describing an earlier version of tautLib.

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!

De-uglification: lifted SAT_cex exception into HolSatLib signature.

Summary: tautLib upgraded to use HolSatLib engine.

Details:
* tautLib signature (and behaviour hopefully!) is unchanged.
Internally, TAUT_CHECK_CONV now uses HolSatLib.
* HolSatLib can now handle Boolean-valued conditionals. This
was forced because tautLib handled them.
* We now have full drop-in support for zChaff, via a proof translator.
* HolSatLib now deletes temporary files.
* Legacy HolSatLib interface dropped in favour of simpler
interface with single entry-point, plus some convenience
wrappers.
* examples/miller/m renamed to selftest.exe; now works with build -selftest
* build-sequence changes: src/compute and src/HolSat/* moved above src/taut;
examples/miller stuff condensed into one entry
* build.sml patched to handle zChaff proof translator (in C++).
* New windows binaries for MiniSat and zChaff proof translator.
* Changes/additions to HolSatLib interface rippled to affected files.
* Documentation updated. In particular, HolSatLib section in Description
had to be almost completely rewritten.
* HOL builds to selftest level 1 on standard kernel, and level 2 on
experimental kernel. Level 2 failures on standard are non-critical
and authors have been informed.

Update this to use the redefinition of Parse structure approach. The
setting of the global grammar approach failed because of the TAUT
function, which referred to Term in its body. By not redefining Term
at the head of the file, TAUT then used the ambient grammar, not
boolTheory's when it parsed its argument. The fix puts things back to the
way they were.
(Of course, there is an argument that tautLib.TAUT should be parsing
its argument with the global grammar, not boolTheory's. If we make this
judgement, then the implementation of TAUT should change to explicitly
pull the global grammars out of Parse, using ambient_grammars, and to
then parse with these.)

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Modified to avoid use of equality on terms in calculation of set of
sub-terms to abstract over.

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.

tautLib.TAUT was parsing with Parse.Term, which could mean that
things intending to be propositions would not parse as such. Parsing
with the fixed bool_grammars fixed the problem.

paired syntax tediosity.

Tediosity.

Irritating changes.

Added ASM_TAUT_TAC, which uses the hypotheses of the goal.

Upgraded to handle overloading.

Initial revision