Fix ARM/v4 example for tight equality

Remove Globals.priming.

Also remove references to it in code that isn't being tested in the
regression checking build-sequence, and so is probably bit-rotted.

Provide numvariant version of variant, which behaves like

with_flag(Globals.priming,SOME "") (variant avoids)

Document change/incompatibility in release notes.

Support for simplifying and evaluating enumerated type representation/abstraction maps.

For example, given

Datatype `enum = one | two`;

the following now works

> EVAL ``num2enum 1``;
val it = |- num2enum 1 = two: thm
> EVAL ``enum2num two``;
val it = |- enum2num two = 1: thm

> SIMP_CONV (srw_ss()) [] ``enum2num two``;
val it = |- enum2num two = 1: thm
> SIMP_CONV (srw_ss()) [] ``num2enum 1``;
val it = |- num2enum 1 = two: thm

This also works when building custom compsets using computeLib. add_datatype_info.

NOTE: This change may break some proofs (some in example/ARM have been fixed).

Don't emit definition bindings for enumerated constants.

Fixes #78.

This commit also

* fixes uses of constructor definitions (the equations are still
present under the "number2<ty>_thm" name)
* provides a regression test
* a bug fix claim in the release notes.

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Repairs: replacing "$-"` with "-".

Fix following changes to wordsLib.

Minor changes.

Remove unused stuff.

Renamed bsubst to update (as it is in v4T).

Moved a few definitions/theorems to better homes.

Remove excessive priming from a couple of definitions.

wordsLib.WORD_GROUND_ss has been dropped.

Have rationalised the treatment cases for words,
changing word_nchotomy to ranged_word_nchotomy.

This means that "Cases" and "Cases_on" now subsume
"wordsLib.Cases_word" and "wordsLib.Cases_on_word".
Have eliminated some occurrences of the latter.

Revised expressions of the form <term>:<type> ' <term> to be (<term>:<type>) ' <term>
to avoid confusion with the type variable ' .

Fixed broken proofs - following addition of WORD_ss to srw_ss().

Also replaced %% with '.

Whoops! Used the wrong file, when I edited slightly to make types more easily parsed, by enclosing in parentheses. This should be the correct version.

Edited slightly to make types more easily parsed, by enclosing in parentheses.

Fix parsing/printing for UMULL etc.

examples/elliptic/arm -> examples/ARM/v4
examples/arm6 -> examples/ARM/arm6-verification