Add a new example: a small verified bootstrapped compiler

This commit contains a development of a "minimal" verified
bootstrapped compiler that targets x86-64 assembly code.

I have added this to the build-sequence as one of the final
examples. The tactic proofs build under both the standard and the
experimental kernels. However, the bootstrap evaluation (in
compiler_evalScript.sml) seems to get stuck on the experimental
kernel. (Is it possible to exclude an example from the build
sequence if HOL is built using the experimental kernel?)