Started working on a module layer.

The first step in getting modules working is to refactor the semantics
of declarations.  In doing so, I'm getting rid of the small-step
declaration semantics, as it was rather pointless.
Finished fixing type soundness for the new evaluate_decs
More progress on the new evaluate_decs definition
Thread a module environment throigh the semantics.
Push a module environment throught the type system.

I used lots of cheats to get the proofs working, because I haven't yet
defined a good module type environment.
Started to work on module environment invariants.
Removing cheats
Changed the semantic's constructor environments.

Previously, the operational semantics kept an environment that mapped
each constructor to all of the other constructors of the same type.
This allowed pmatch to determine whether the construcor value matched
against a constructor pattern were of the same type (relying on the fact
that there were no duplicate constructor definitions).  Now, the map
just stores the type that the constructor comes from and pmatch can do
the check directly.
Removed more cheats.

There is one remaining cheat, and the cheated lemma will need a stronger
precondition about data constructor uniqueness to be true.
Expression-level type soundness works without cheats.
Started fixing the evaluate and evaluate' proof
Get ml_translatorScript.sml working for the new expressions.
Comments
Fix a script that became broken with some recent changes to HOL.

This probably makes the script not work on older versions of HOL :(
Some intermediate stage of getting modules working
Work in progress on modules
More progress on modules.

The semantics and type system is (mostly) there, but the proofs now all
need maintaining and extending.
Get untyped safety and determinism working for modules.

Also using a newer version of Lem that makes the spacing worse for the
generated HOL.  Hopefully this will be fixed soon.
More progress of module type soundness.
More progress on the module system.