Make global simpset state easier to recreate with "logged_update"

This entry-point records that a change to the global simpset has
happened within a piece of code (rather than a script). The change is
made (as before), but the change is also recorded so that it can be
recreated/applied to different base simpsets.

Add conversion INT_WORD_GROUND_CONV.

Support building custom compsets that cover bitstringTheory and integer_wordTheory.

Add a new theorem about bit-vector overflow.

Includes an improvement to the Cases_on_i2w tactic.

Added new definitions and theorems for various bit-vector "saturation"
operations.

These operations return maximal or minimal values instead of, e.g.,
overflowing (wrapping). For example:

|- signed_saturate_add 100w 50w = 127w: thm

Also added a new configuration option for printing word literals as 2's
complement values. For example:

> set_trace "word pp as 2's comp" 1;
> ``253w:word8``;
val it = ``-3w``: term

Be warned that this term is actually ``n2w 253``, it's just being printed as
``word_2comp (n2w 3)``.

This printing mode is useful when checking the veracity of machine arithmetic.
For example:

> EVAL ``signed_saturate_sub 226w 100w : word8``;
val it = |- signed_saturate_sub -30w 100w = -128w: thm

Missing boolLib.

Assorted extra theorems and tools. Added a new constant word_abs, which gives
the absolute value of a bit-vector.

Fix following change to wordsLib.WORD_DP.

Adds integer_wordLib.WORD_DECIDE (which is based on COOPER_PROVE). This
provides a faster version of wordsLib.WORD_DECIDE.