Fix theories in arm6-verification/correctness

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.

A minor fix to make this script work with the recent change to
parse_in_context. Unfortunately, this directory doesn't build, at
least under the experimental kernel.

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.

The ARM6 example was failing to build (thanks to Hasan for spotting this).

The problem stems from changes made to the evaluated of w2w.

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