Added parsing of SMT-LIB decimals as real numbers.

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

Made "and" and "or" right-associative. The alternative of making them left-
associative interacts badly with the existing implementation of Z3 proof
checking.

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.