revert some of 0fc7587: allow add_persistent_funs of other consts

change interface to add_persistent_funs (#73) and fix more calls

The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.

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

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 following Michael's takeover of "U".

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!

Test out using using unadorned underscores in case statements.

Also added derived theorems for "ADD rd, pc, #n" and "SUB rd, pc, #n".

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

Moved a few definitions/theorems to better homes.

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

Also replaced %% with '.

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