Patch for minisat sources.

This was failing to build on Mac OS.

For some reason the MacOS g++ was not #including sys/types.h in
response to the given program text, but the Linux version was. By
explicitly mentioning it, things compile again on both systems.

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.