Reformat to remove lines longer than 80 columns in src/HolSat

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!

* 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.

Some technical improvements:

* HOL-side
- All is now tail recursive and most uses less RAM
- Undocumented feature allows skipping CNF conversion (still WIP)
- General refactoring preparatory to adding proof replay for ZChaff
* Solver-side
- Proof log now indexes root clauses, and writes sign info for pivots
- Proof::compress has been implemented
- Folded in miscellaneous upstream deltas

PS: None of the above applies to defCNF stuff. Still a black box to me.

* SAT_TAUT_PROVE now returns counterexample theorem in case of failure.
* SAT finding using MiniSat now works as expected
* Speed improvements backported from my HOL Light port

Removed unused stuff from satCommonTools.sml. Minor knock-on effects.

Cosmetic fixes so we can move up the build sequence.

HolSatLib refactoring and additions.

* MiniSat-p v1.14 added as a "built-in" SAT-solver
* A new function SAT_TAUT_PROVE uses MiniSat to prove propositional
tautologies within HOL
* HolSatLib refactored into satTools and dimacsTools
* Local documentation removed; it was folded into the
Description some time ago.
* The HolSatLib interface remains the same, save for the addition of
SAT_TAUT_PROVE.
* Two minor additions to defCNF: a global ref for the variable name
prefix used by DEF_CNF_VECTOR_CONV (defaulting to the current setting),
and a global ref for the number of new vars introduced by definitional
CNF.