Added support for Z3's proof rule IFF_TRUE.

Using our own syntax for th-lemma (Z3 proof syntax for it is just broken).

Added parsing support for bvurem0. Fixed parsing of bvudiv0.

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

Added parsing support for ~, bvurem_i, bvudiv0, repeat<n>, rotate_left<n>.

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

Added a parser for SMT-LIB 2 benchmarks.

Rephrased a speculative comment, based on feedback by Michael Norrish. Some
cleanup.

Toward parsing of Z3 2.12 proofs.

Fixed a compilation error.

Proper parsing of xor and array_ext; minor rephrasing.

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.