Remove TABs from examples

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.

Comment out generation/emission of ML code for SHA-1 and TEA. The
emitted files were bogus, and caused compilation to fail in
src/emit/ML. This latter directory isn't normally compiled at all,
but the ordinal example is set up to depend on it, so it ends up being
compiled when Holmake calls itself recursively.

Half get this to work. Though it compiles, and proves its theorems,
it's not exporting its ML correctly, complaining about there not being
a binding for words$n2w. I guess I need to replace the
WORDS_EMIT_RULE that I removed with something else...

Update to using wordsTheory.

Moving SHA-1 example into Crypto directory.