Added support for Z3's proof rule IFF_TRUE.

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

Checking Z3's rewrite proof rule now uses bit-blasting as a fallback.

Added a parser for SMT-LIB 2 benchmarks.

Some cleanup. Stricter error checking, separate profiling function.

Various changes, notably to rewrite_nnf, ALL_DISTINCT_CONV, rewrite, and
th_lemma_bv. Work in progress.

z3_monotonicity can now handle inferences that require rewriting the lhs from
``x /\ y ==> z`` into ``x ==> y ==> z``. These are arguably a bug in Z3 2.11,
as they go beyond the documented capabilities of the monotonicity rule.

Refactoring and minor cleanup.

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.

Using BBLAST_TAC (just trying it after everything else for now; further tuning
necessary).

Further tuning of bit-vector proof methods.

Further minor enhancements for bit-vector proof reconstruction.

Replaced WORD_ARITH_EQ_ss by WORD_ARITH_CONV (which also fixes the sign of word
equalities); also added this conversion to the implementation of rewrite.

th_lemma now uses WORD_ARITH_EQ_ss (to prove further theorems involving words).

Array updates that use word literals as indices are now dealt with, both in
rewrite and th_lemma.

Towards proof reconstruction for bit vectors.

Augmented unit_resolution so that it can eliminate ``F`` disjuncts, as in

p \/ F
------ unit_resolution
p

Tuned (replaced String.concat o Lib.separate by String.concatWith).

Z3's proof rule true-axiom implemented.

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

HolSmtLib now supports the Z3 2.0 proof format.

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