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

The overloading of %% onto fcp_index has been removed in a previous check-in.
This was to free up the symbol, which has be replaced by the preferable '. It
is easy to restore the old overloading locally, if required.

Fix handling of special 'U' constant, retaining better backwards compatibility.

In particular, there is now a special form 'univ' that behaves as 'U' did.
Further, with Unicode on, the character U+1D54C is used in the same way.
This character may not be in many fonts, so add another trace to turn its
use off. If you can see it, it's a nice 'double-struck' U. I would have
gone for a script-style U, but it leant over too much, and so overlapped
the following left-paren character.

Make U syntax for UNIV consistent in its parsing and printing.

Now you can write FINITE U(:'a), and it parses. This used to require
FINITE (U(:'a)), which is so many parentheses that one wonders about the
usefulness of the abbreviation.

Fix for another ARM script that wants to use "U" as a variable, not UNIV.

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