Add some SSE (streaming SIMD extensions) instructions to the x86-64 model.

Remove eqtype declaration for term type

Minor updates for the x64 model.

• The decoder has been tweaked (mainly for use under SML). Previously it would succeed in decoding an instruction even if there were too few bytes.

• x64DisassembleLib has been removed. The function x64_disassemble has been implemented in x64AssemblerLib.

Various updates to the L3 examples.

Most changes are brought about by improvements and generalisations within stateLib and utilsLib.

A Holmakefile has been added to a new decompilers sub-directory and some *decomp_demoScript files have also been added. This makes it easier to perform regression testing.

Simplify the x86-64 model under L3 examples.

The instruction cache has been removed, together with the CPUID instruction. Also, the memory now has type ``: word64 -> word8`` instead of ``: word64 -> word8 option``.

Improve the interface to stateLib.update_frame_state_thm.

Also add some explanatory comments within stateScript.sml.

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.

Update for x86-64 model and tools.

- x64Theory now includes an instruction encoder.
- The functions in x64_stepLib have been renamed, e.g. x64_step is now x64_step_hex.

Simplify tracing for the x64 spec function.

Add support for x86-64 assembly code.

Based on NASM syntax, as opposed to AT&T (which is the default for gas).

Updates for machine-code tools.

Added support for introducing SEP_ARRAY predicates for memory operations (applied to the ARM and M0 models).

Update x86-64 tools to support generation of TEMPORAL triples.

Update M0 tools.

Minor updates to other ISA tools.

Updates and improvements to the l3-machine-code decompilation tools.

Further updates to the tools linking the L3 ARM model to the decompiler.

A lot of code has been generalised (making it usable with other models) and the performance has been improved.

The Hoare-triples for PC-relative loads now have immediate values appearing in the code-pool.

This affects the triples that are generated for instruction such as "ldr r1, [pc, #12]".

The tools for the other ISA models need minor updates following changes in stateLib.

Support symbolic immediate values in x86 (L3) tools.

Extend L3 x86 model with support for MOVSX instructions (move with sign extend).

Missing files from last commit.