update parser to handle string literals

and fix soundness and completeness proofs.
string literals parsed to a new AST entry for Lit.
Merge branch 'master' into strings

need fixes to Holmakefiles to make building easier
add strings to type system and inferencer

update metatheory and inferencer soundness
add string printing to the repl semantics

including string_escape (not sure if that already exists somewhere).
rename String constructor to StrLit

to avoid clash with the Lem module called String
compilation of string literals

tests don't work because of problems with Lem's and EmitML's support for
strings vs char lists; will require some hack. proofs not looked at yet.
compiler tests build
touch up compiler proofs for strings

although cheat the case about correct compilation of strings, and
haven't added the new clause to the data refinement relation either.
add strings to data refinement and observable values

remaining tasks at least include: prove cheat about compilation of
string literals, and update implementation of bytecode Print
instruction. but might skip the latter since we might want to soon get
rid of the Print instruction...
prove correctness of compilation of strings

now compiler proofs all build. should check repl next.
fix replCorrect for strings
add missing case to tc_to_string for TC_string
temporary hack translation of int_of_num

it shouldn't be translated at all
fixes to bootstrap_lemmasScript.sml for strings
translate (int_of_num n) properly, but still fails

because we actually need to translate f o int_of_num and int_of_num o f
attempt to translate combinations of int_of_num with other funs

now translation of compile_top fails in a less understandable way...
fix bug in translation of $& o f and f o $&

now ml_repl_stepTheory compiles fine
Merge branch 'strings'

breaks x86-64 because printing is not updated. but the plan is to
attempt to change the way printing works (in particular, make it
type-directed) first.