zDefine and_shadow to avoid ThmSetData.revise_data warning message
prove cheat in replCorrect'_lem

reworked proof a little bit to use both conclusions of the IH
prove last cheat in replCorrectScript.sml

(about initial bc state satisfying code_labels_ok and code_executes_ok)
Work on the unverified implementation

Move the lexer to use Parsec and so be able to track source locations.
Merge remote-tracking branch 'origin/x64'
some cleanup in compiler/bytecode
some cleanup of compiler/proofs

superficial pass, up to but not including toBytecodeProofsScript.sml
some cleanup of toBytecodeProofsScript.sml

just moving things around; haven't tried speeding up or shortening
proofs yet.
Delete some unnecessary tokens.
a cleanup pass on compilerProofsScript.sml
Fix a place where inference was overconstrained

e handle ...

required that e have type int.  Fixed now.
Error messages for the unverified implementation
another cleanup of compilerProofsScript.sml

mostlty moving stuff out into earlier theories
Finished type error messages
move bytecode directory to top level
top-level README tweaks

including adding unverified
move inferencer to top-level directory
reorganise implementation directories

implementation is now repl; impl_proofs is now repl/proofs.

bootstrapping is moved to a new top-level bootstrap directory.

The bootstrapping-correctness proofs are moved to translator/repl/proofs.
They no longer depend on the actual bootstrapping; rather they talk
about "whatever the result of compile_decs oneshot is".
We might want to make an instantiated version under bootstrap/proofs, though.
rec Equal verified
Merge remote-tracking branch 'origin/master' into x64