Start removing the elaborator

Moving its remaining functionality into the type system itself.
Merge remote-tracking branch 'origin/master' into remove_elab
Semantics builds
Progress on type soundness
Merge remote-tracking branch 'origin/init_env' into remove_elab

Conflicts:
	semantics/replScript.sml
	translator/Holmakefile

Further development of the removal of the elabotator needs to take into
account that the initial environment has changed
metatheory builds
Progress on type inference

But not quite there yet.
Inference builds
Actually remove the elaborator
Type abbreviations completed

The initial program is now has bindings, e.g., (Dtabbrev [] "int" (Tapp
[] TC_int)), that replace the functionality of the elaborator. But now
these work in modules too, so, for example, Word8Array.elem is a type
abbreviation for (Tapp [] TC_word8).

metatheory and inferencer soundness build, but nothing else is tested
yet.
Add a HOL heap to bytecode

To speed up its build. Basing the holheap on the semantics one. Somehow
this changed HOL's state so that a few proofs brokd showing that w2n x <
256 for an 8bit word. Used WORD_DECIDE_TAC to prove those.
Compiler proofs build with 1 cheat

In printerScript.sml for the case of printing a declatation that is a
type abbreviation. Nothing is printed, so this should be an easy cheat
to fix.
Some progress on compiling the initial env
prove cheat in printingScript.sml
Get repl_fun to build
Merge remote-tracking branch 'origin/init_env' into remove_elab
Some progress on replCorrect
Fix replCorrect
Merge remote-tracking branch 'origin/init_env' into remove_elab
Fix translator