fixed parse_Z3_version() for 64-bit Z3

Z3 solver won't attempt proof replay if version <> 2

HOL4_{YICES,Z3}_EXECUTABLE evaluated at run-time (as opposed to compile time). Minor refactoring.

Made location of Yices and Z3 executables configurable. This allows to work
around issue #87.

More liberal (elegant, portable) treatment of whitespace.

Added support for Microsoft Windows-style newlines (\r\n).

Added -file: to the Z3 command line (to simplify external post-processing, in
particular for Z3 under Wine).

Added support for LET terms to the SMT-LIB translation. (Proof reconstruction
for Z3 still requires unfolding of LETs.)

Fixed abstraction of higher-order goals into first-order formulas.

Added SmtLib support for word shift by number (via simplification).

Added (partial) support for shift operations that take two word arguments.

Major update, adding a translation from HOL to SMT-LIB 2 and enabling Z3 proof
checking again. (The latter still has some quirks, because Z3's proof
syntax is not fully SMT-LIB 2 compliant.)

Major update, adding support for Z3 2.11 proofs (SMT-LIB 2 format).

Note that this breaks Z3 proof checking from HOL4 (for now), as no translation
from HOL4 into SMT-LIB 2 has been implemented yet.

Moved various auxiliary theorems from SML source files into a separate theory
(script file), following a suggestion by Magnus.

Tuned.

Temporary files are now created in the temporary directory (i.e., /tmp on Unix)
and no longer re-used between separate SMT solver invocations.

HolSmtLib now supports the Z3 2.0 proof format.

Z3 proof reconstruction split up into separate files. Minor other changes.

Simplified the interface to provide tactics only (use Tactical.TAC_PROOF or
similar to derive functions of type goal -> thm). Also simplified the
discharging of definitions in theorems derived by Z3.

Changed the interface to take a goal (i.e., a pair of assumption list and
conclusion) instead of a single term.

The same interface is provided by the SMT-LIB standard, which distinguishes
between assumptions and query formulas, and claims that "many SMT solvers can
process assumptions more efficiently if they are explicitly identified as
such." I don't know if that's true, but in any case, identifying them
explicitly is what we do now.

Removed some comments (containing alternative implementations of unit resolution
that had shown inferior performance).

This is a major update, adding proof reconstruction for Z3 (and several smaller
improvements).