use new compset fragment in HOL's examples/parsing
generate smaller Theory.sig for ml_repl_step
update sideTheory

not sure if things need to be added to it, but repl_step_side is proved
(and dependencies).
some new Lem-generated files

this slightly broke one proof due to a change of bound variable names
remove probably useless bring_to_front_overload"Num" from cakeml_compute

I didn't see any occurrences of "Num" in the file, so I presume this
isn't necessary any more. If it is, it should be the temp_ version since
this is not a script file.
make dependence on $HOLDIR/examples/parsing explicit

for pegLib which is used in cakeml_computeLib

this might be picked up transitively (through heaps) via the dependence
on ../parsing, but that seems to be a bit flaky
start updating bootstrap/Holmakefile

this commit makes it something more reasonable given all the changes
since bootstrap was last touched, although it may still need further
tweaking
tidy use of SUC_TO_NUMERAL_DEFN_CONV in cakeml_computeLib
use sLet_pat_thm rather than _def in cakeml_computeLib

the former is a small simple definition, whereas the definition has
unwieldy pattern-matching. probably the nice theorem should move into
compilerTermination or something so it doesn't depend on the proofs, but
this works for now.
move sLet_pat_thm into compilerTerminationTheory
save theorems precomputing evaluation of real_inst_length together

previously had generated a separate theorem for each case and added them
to the_compset. it makes more sense to save a single theorem (the
conjunction) so it's easier to find it to add it to other compsets.
use eval_real_inst_length for code_labels_conv in cakeml_compute

labels_computeLib.code_labels_conv needs a conversion to evaluate the
length function. previously had been passing in the cakeml compset
evaluator, but this doesn't include evaluation of real_inst_length. it
actually probably makes more sense to use a conversion that is
specialised to evaluating real_inst_length, so that is what we do in
this commit. if it needs to become more versatile later (e.g. for other
instruction lengths) we could make eval_real_inst_length a reference.
add some missing defs to conLang part of cakeml compset
initial experiments bootstrapping repl_decs

on a basic evaluation using the cakeml compset the time starts to go
badly non-linear after about 100 decs, which is around when the type
inferencer and rest of compiler start being defined. will probably need
to resort to some of the tricks used last time, namely splitting the
decs up into chunks and doing something smart with finite map lookups.
possibly other optmisations are possible too.
make evaluate_prompt_i1 check for duplicate module names
prove a version of prompt_to_i2_correct

A cheat-free version of this theorem (for once). Uses the old envC in
the case of an exception, so it might require some tweaks further up in
compile_top/prog's theorems. Not sure if all the assumptions on this
prompt_to_i2_correct are strictly necessary.
prove evaluate_prompt_i2_exh_weak

needed to add assumption about non-type-error
remove unnecessary assumption from prompt_to_i2_correct

this is perhaps a bad sign: we don't need to assume that a prompt of
SOME mn only makes declarations of things with module mn.
failed attempt to prove prog_to_i2_correct

comment it out entirely for now: need to find out whether the current
prompt_to_i2_correct is good enough, and also what exactly is needed
from prog_to_i2_correct.
Merge branch 'master' into conLang_wip

Conflicts:
	miscScript.sml (trivial)