Start on user-defined exceptions

Update the semantics for raising and handling user-defined exceptions,
but not for defining new ones.  My changes to the grammar and ptree
conversion are just best guesses that I'm not confident in.  I also
added cheats to terminationScript because changing the AST makes HOL
renumber the size functions, breaking the proofs there.
Fixed the invariant definitions and bigClockScript
Adjust grammar and PEG for proper exception-handling syntax.

Soundness proof fixed also. Tests not yet checked because of unrelated
lexing bug.
Merge branch 'master' into exn
Further fixes to grammar for exception handling.

Remove Exn non-terminal. Tests don't pass, and completeness doesn't
build either. Soundness is good though.
Merge branch 'master' into exn
Changed the way handle works in the semantics

Instead of doing an evaluate_match on the (pat*exp) list with an added x
=> Raise x pattern at the end, just add an extra argument to
evaluate_match saying what it should raise if it runs out of patterns.
Case can give it the Bind exception and Handle can give it whatever
exception it tried to handle.
fix some stuff in the semantics terminationScript.sml
update compiler for new exceptions, untested

tests and proofs likely broken; waiting on metatheory before running the
tests.
Fix the big/small-step equivalence proof
Fix two more scripts

There a cheat in untypedSafetyScript for a case where I haven't made the
definition yet
TypeSoundScript builds, but with 16 cheats in it
metatheory builds, but with lots of cheats
Added cases to the semantics for exception declarations

And got most of metatheory building with no cheats.  Only the
alternative big step semantics is broken, everything else works.
Metatheory builds again

But with a few cheats in bigBigEquivScript.sml
Actually "fix" bigBigEquiv
Some progress on bigBigEquiv
Finished the metatheory directory for exceptions.
Get the inference algorithm updates, and the proof building

4 cheats
Adjust grammar to remove problem with fn V => E inside case expressions.

PEG adjusted, and soundness reproved.