Add a variety of rewrites to the stateful simpset

Get src/integer to build given tight equality

Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Add theorem w2i_eq_0.

Improve/add some word theorems.

Simplification theorems for wordsTheory and integer_wordTheory.

Remove Unicode under src/

This problem is now being spotted by self-testing again, thanks to
c529f76

Fix integer theories in light of pat_assum rename

Add various theorems from CakeML

Remove cheat that I'd forgotten about

Add a few theorems to integer_wordTheory

Opening lcsymtacs is no longer necessary.

Tweak definition of integer_word$fromString.

Move n2l and l2n constants (and similar) into new numposrep theory.

A number of fixes follow on from this.

Also mention the new theories (numposrep and ASCIInumbers) in the release notes.

This is progress with #70.

Add a new theorem about bit-vector overflow.

Includes an improvement to the Cases_on_i2w tactic.

Add toString and fromString to integer_wordTheory. Also, make improvements to syntax files.

Add word_sign_extend to words emit + minor cosmetic changes.

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

Remove some Unicode that has crept into scripts.

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

Added new theorems: WORD_EXTRACT_OVER_ADD and some for addition/subtraction
wrt integer_word$i2w.

Implement unary minus (the old ~ still also works). Selftest level 2
passes. Changes in the "words world" were replacing $- with -. In
the two quotient changes, I made sure that the infix operator
that used the - character was part of the grammar before it was
parsed. This is necessary because - is now a non-aggregating
character, mainly so that ``--p`` parses as three tokens, not two. Of
course, if you added -- to your grammar, then it would go back to
parsing as two.

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

Emit ABS.

Tweak spacing.

Add integer operations to EmitML.

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Added theorems for the signed-word orderings.

Thanks to Michael's last check-in, index types are now directly
supported by the parser/printer, so there is no need to introduce
the "iN" type abbreviations.

Some minor changes to the code generated by EmitML. DIV_2EXP is moved to
arithmeticTheory, so that is can be included in numML.

Added theoryML/mlton/numML.sml, which supports fast arithmetic when
using MLton.

Moved DIV2 and MOD_2EXP to arithmeticTheory. This enables the numML.num
data type (wrt EmitML) to be abstract -- without the big slowdown caused
by the lack of numeral versions of these functions when running the ML.

Apologies, have done some renaming:

TOP -> dimword
MSB -> INT_MIN

Also added UINT_MAX and INT_MAX.

word_L, word_H and word_T have been overloaded with
INT_MINw, INT_MAXw and UINT_MAXw.

Alter the n-bit word theories to use the :'a itself type, and also add
new constants (TOP(:'a) and MSB(:'a)) to stand for the numeric value of
2 ** width, and 2 ** (width - 1). Using these makes the expression
of several results a lot nicer. As the updated proofs in integer_wordScript
demonstrate, you don't always have to expand these definitions either,
which is nice.
I'm not 100% sure that these are the best names for these constants.

Some more theorems about integer modulus, allowing a slightly nicer proof
in integer_wordTheory.

Another theorem, about where integers have to fall to make the sign-bit
set in the corresponding word.

More theorems, including the useful w2i (i2w i) = i (as long as i is in
the reasonable range)

Start of a theory relating fcp-words to integers.