Some minor updates to the x86 semantics and the compiler.

Many minor updates.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

A general update:
1. the decompiler is now slightly faster, due to new code
abbreviations (terms smaller in internal proofs);
2. the definition of the machine-code Hoare triple
was slightly altered to support instruction caches;
3. the x86 model now includes an instruction cache.

Also, I give up on attempting to support MoscowML for
examples/machine-code/lisp. Both the standard kernel and the
experimental kernel crash while loading files in this
directory using the latest patched version of MoscowML.
Both kernels exit with an uninformative message:

Compiling lisp_equalScript.sml
Linking lisp_equalScript.uo to produce theory-builder executable
Uncaught exception: Chr
Failed to build script file, lisp_equalScript

Did they run out of memory? If so, why does the error message not
say so?

Restructuring and simplification.

A new version of files previously in examples/mc-logic.
Eventually examples/mc-logic will be deleted.