Added parsing support for SMT-LIB's define-fun command.

set-logic is no longer expected to be the first command (in accordance with the
SMT-LIB standard).

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

Z3 proof parser updated for Z3 2.13. The proof parser now uses the SMT-LIB
benchmark parser internally.

Fixed yet another compilation error. Added support for line comments (;...\n)
to the SMT-LIB parser.

Added a parser for SMT-LIB 2 benchmarks.

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.