make mlstring_case_conv slightly more robust/lenient

attempt to prove that the lhs of the generated theorem is equal to the
input term, rather than just failing if it isn't aconv
add better mlstring_CASE handling to translator

also had to use the classic pmatch heuristic to define TRANS and MK_COMB
in the HOL Light kernel because the default heuristic makes a case
expression that is too complicated for my mlstring_case_conv to deal
with
Add string and character stuff to the basis

Committing to a branch, because it breaks the build. The necessary
theorem that the basis evaluates to SOME rather than NONE no longer
proves.

Ideally, this theorem could be proved by evaluation, but you run into
the following problem.

Suppose that we have

val f x = 1;
val g x = 1;
val h x = 1;

Then after f, the environment is

(f|->Closure [])

after g, it's

(g|->Closure [(f|->Closure [])]),
(f|->Closure [])

and after h it's

(h|->Closure [(g|->Closure [(f|->Closure [])]),(f|->Closure [])]),
(g|->Closure [(f|->Closure [])]),
(f|->Closure [])

As you can see it grows exponentially, although there is the possibility
of sharing since each Closure simply duplicates the environment as it
stands. Possible fixes:

1) Alter the semantics so that there is a heap for environment frames to
go in. Then the semantics itself can express the sharing. This would
probably complicate the translator and any future reasoning about CakeML
programs.

2) Make a super smart EVAL that keeps let bindings at the top of the
term to capture the sharing. So when you're about to put (f|->Closure
[]) into g's closure, you go to
let frame1 = (f|->Closure []) in (g|->Closure [frame1]),frame1
This is the shallowly embedded version of 1. It seems hard, but might
be of general use.

3) Make another interpreter for CakeML that does 1, but then have a
custom conversion that maps the heap-threaded environments onto normal
environments using the let technique of 2 to maintain all of the
sharing. I worry that this is more work than it's worth.
add theorem about location of i/o ptrs in the globals
fix proof of basis_sem_env_SOME

just using abbreviations within the tactic proof, c.f. issue #6
Merge remote-tracking branch 'origin/master' into string_basis
start on restricting argument to generated PushInt instructions

that is, issue #5. updated the compiler and proved a general theorem
about the push int code generator, but haven't fixed the proofs where
that theorem now needs to be used.
update holSyntaxSyntax for change to Abs

it takes two terms rather than a destroyed variable and a term
update compile_varref_thm for PushAnyInt
fix prim1_to_bc_thm
finish updating bytecodeProofTheory
Merge remote-tracking branch 'origin/master' into PushAnyInt
add PushAnyInt stuff to compiler compset
add support for translating integer negate
prove side conditions resulting from PushAnyInt
add phony "all" target to various Holmakefiles

to recreate the default behaviour of Holmake after recent changes in HOL
make it only build the first target in the Holmakefile if one exists
(and it often does for us: the HOLHEAP).
Some updates for the machine-code backends.

Conditional jumps now have their own offset limits. This has been promoted by ARMv8 where the range of conditional jumps is less than that of regular jumps.

The encoding size restriction for instructions with offsets is now more liberal. Before, encoding lengths could not vary with the size of the offset. Now the encoding lengths are required to be monotonic with respect to the magnitude of the offset. Although this opens up the possibility of using short jumps on x86, this hasn't been implemented.  However, the range of Loc instructions for ARMv6 has been increased: from 8 bits to 16 bits (via two instructions).

The length of Skip instruction encoding is now required to be equal to the code alignment value.
fix reference to non-existent parsing-heap

it was renamed to the standard 'heap' at some point
Start on sketching inference completeness for declarations
remove a cheated unused theorem

I think it might be false anyway: what if uv occurs in t?