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.

Attempt patch for issue #103.

Allow Moscow ML build to happen using (as yet unreleased) v2.10.

Basic strategy is to make adoption of basis 2002 even more
thorough. In particular, the Timer structure is now as per
the 2002 Basis.

It is possible to detect that one is working with Moscow ML 2.10 or
later by checking the Holmakefile variable $(HAVE_BASIS2002), which is
set (to value "1") when in 2.10 or later. It is unset elsewhere. See
an example of its use in help/src-sml/Holmakefile.

More corrections required to our sources when I do the migration to
Basis 97 properly.

Compatibility fix

Changed occurrences of Process to OS.Process (fixes broken build).

It turns out I couldn't use Systeml.systeml directly as it cleverly
quoted the > meta-character from disturbing the shell. Unfortunately,
the calls to the external tools use file redirection, so this need to
be allowed to pass through. So the use of Systeml resources needs to
be fiddlier.

Change interface to underlying tools to not use Process.system, and to
instead use Systeml.systeml, which can protect against paths that
include spaces and other meta-characters.

* Closed a loophole in HolSatLib failsafe mechanism.
* Replaced MiniSat's DIMACS parser with my own to avoid
build dependency on zlib, which HolSatLib does
not use. Thanks to Anthony for motivation. Updated
docs.

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.

Update the type of mk_oracle_thm so that it takes a string rather than a
tag as first argument. This is to prevent the following scenario:

- show_tags := true;
> val it = () : unit

- val ax = new_axiom ("foo", ``T``);
> val ax = [oracles: ] [axioms: foo] [] |- T : thm

- val th = mk_oracle_thm (Thm.tag ax) ([], ``F``);
> val th = [oracles: ] [axioms: foo] [] |- F : thm

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

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.