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.

Word slice "<>" has been replaced with "''".

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!

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.

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