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

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

De-uglification: lifted SAT_cex exception into HolSatLib signature.

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

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.

MiniSat added to list of supported SAT solvers.

Had to suppress failure warning for MiniSat by special-casing, because it returns a non-standard exit status code.

Trying to sync everything (not sure why HolSatLib.sm is here)

Added initial version of HolSatLib