bit more progress on add_constraints_thm

reduced to showing that the constrained interpretation still satisfies
the axioms in the original context.
bit more on add_constraints_thm

Need something like semantics_extend but going in the other direction:
if you satisfy something in an extended signature then you satisfy it in
a reduced signature. The problem is satisfaction in an extended
signature looks weaker because it quantifies over fewer valuations. But
I think this shouldn't actually matter...
rename broken word_preludeScript.sml so it doesn't get built
rename the heap used for translator examples

and uncomment it for okasaki-examples
Add some Lib files under targets.

The facilitates the evaluation of x64_enc.
Add a theorem decoder_asm_deterministic.

This theorem provides a means of showing that asm_step is deterministic via the use of a suitable decoder (witness).
rename various translator/other-examples that depend on word_prelude

the problem with word_prelude is that the translator gets confused about
whether to use the built-in WORD8 refinement invariant for word8, or the
(admittedly poor) WORD refinement invariant defined in word_prelude. the
right way to fix all this is probably to add proper support for word8
operations to CakeML, and just use WORD8 everywhere.
finish proof of add_constraints_thm

add two lemmas to help:
  subterms of a term_ok term are term_ok, and
  it's possible to extend a valuation to a larger signature
Put get_token_def back into compset for parsing/testing (only)

This stops the infinite loop that was occurring when cmlTestsTheory
built.
Better fix for parsing/testing, by inheriting from lexer_impl

This relevant ancestor theory wasn't being used, and so the test-suite
missed out on the changes made in 02d4772a.
Update HOL URL in README.
Moved added datatype def out of comments
delete out-of-date compiler tests

There may be some interesting small example programs here, but the AST
they are written in is quite out of date and using the parser on tests
written in concrete syntax is probably a better approach for the future.
There is also some broken infrastructure for putting the compiler
through EmitML, but using the translator is a better option for that.
Bugfixes after the order of default globals changed
Add missing defs to compset
Fixed pretty printing of function types as it is now eval-ed
Used the terminating version of subst in compute_semanticsLib and remove a superfluous case in proof
Added missing defs to compset for type inference on signatures
make build-email.sh send email in case of success too
Merge remote-tracking branch 'origin/master' into fmap_refactor

Conflicts:
	initial/initCompEnvScript.sml