Fix src/HolSmt/Library.sml so that it compiles again.

There is far less 'open' in Library.sml than is typical.

Improve HolSmt's coverage of bit-vector problems.

This involves mapping some HOL bit-vector operations into suitable SMT-LIB
operations. In particular, provide support for:

1. reduce_and, reduce_or, etc. This is done using wordsLib.EXPAND_REDUCE_CONV.

2. word_lsb, word_msb, word_bit, word_bits, word_slice and bit_field_insert.
This is done through rewrites.

3. (w2w:'a word->'b word) and (sw2sw:'a word->'b word) where the word size
decreases. Again done using rewrites.

4. ((h >< l) w) : 'a word, where 'a word is larger than h + 1 - l. This is
done using wordsLib.EXTEND_EXTRACT_CONV.

Strings are unquoted during parsing.

Tabs are treated as whitespace (in accordance with the SMT-LIB standard).

Added word_lsl_bv (<<~) to the Yices translation. Added corresponding self-tests.
Disabled word simplification for now, and added tracing output for the
simplified goal.

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

Minor refactoring; replaced = (on terms) by Term.aconv.

Replaced = (on terms) by aconv.

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.

Some cleanup. Stricter error checking, separate profiling function.

Simplification of lsl/lsr when the index is at least as large as the word length.

Added word simplification to YICES_TAC (mainly to simplify expressions of the
form "w2n (n2w n)"; this was a feature request by Yogesh Mahajan).

Added unfolding of LET.

Better support for sets as predicates in HolSmtLib, replacing {x | P x} by P.

Towards support for sets as predicates.

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.