another attempt to get useful output from travis build

need to find the directory in which the regression test script generates
the timing and regression logs
turn off timing.log for travis
move some more theorems to semantics/proofs
Results of hacking during travels: BVI, consts, word_lang

Most importantly:

 - BVI is a new intermediate language that aims to compile the globals
   state component to a dynamically extended wide ref; compiles Handle
   into Call with handler attached; integer const creation is
   shrunk. BVI is a stepping stone between BVL and BVP, i.e. the
   compilation will eventually be BVL --> BVI --> BVP.

 - bvl_const, bvp_const scripts implement certain forms of constant
   propagation (even through GC points). The optimisations are defined
   and to some extent verified.

 - A first draft of word_lang has been defined.

The files build, but many of them are still work in progress.
Merge branch 'master' into init_env
fix for some theorems that moved to evalPropsTheory