Use cached build of Poly/ML and HOL for Travis regression
rework so travis gets its own version of the regression test

which produces more output on stdout (rather than writing to log files)
there is some repetition of code here, but bash is not the best language
for writing things nicely...
fix proofs of side conditions of REPL translation

needed to eta a higher-order call to MAP in build_ctor_tenv_def, and
prove some extra conditions in the type inferencer. apart from that,
some things just got more arguments.
Merge branch 'master' into init_env

(to get better travis behaviour)
fix a proof and make it somewhat more robust

don't know why the order of the subgoals changed
Merge remote-tracking branch 'origin/init_env' into alpha_vector
suppress lem renaming in semantics
prove a version of compile_initial_prog_code_labels_ok

but restricted to the local_labels. something in initialProgram wanted
to use this theorem, and it will have to bridge the gap between
local_labels and all labels (probably by knowing that VfromList code is
in context).