Fix arm6-verification/correctness example for tight equality

Fix theories in arm6-verification/correctness

The overloading Tw is now temporary within wordsTheory.

Put GENLIST computation with numerals back into automatic simpset.

This broke one proof of Anthony's that didn't want
GENLIST f 16
expanded (for good reason). Fixed it by abbreviating the 16 into a
variable.

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!

In preparation for making the standard kernel build under Poly/ML, removed the dependency of src/0/Term.sml on the Moscow ML library Polyhash, replacing this with RedBlackMap.

The building of HOL appears to be faster with RedBlackMap.

Also revised RedBlackMap.sml, RedBlackSet.sml, and HolKernel.sml to eliminate some annoying warning messages.

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