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.

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!

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.

* Implicit definitional CNF (from HOL Light code due to John Harrison),
modified to exploit primitive CONJUNCT* rules in HOL4.
* Optimisations to above for the case where problem is already CNF. This
is handy for SATLIB problems.
* Fallback to SML DPLL prover extended to the case where MiniSat binary
cannot be found or cannot be executed.
* SML DPLL prover modified to use implicit def CNF, and to produce
countermodels in the same format as SAT_TAUT_PROVE.
* Explicit definitional CNF and normalFormsTest files removed, so we can
move HolSatLib up the build-sequence, to follow src/taut.