Avoid some "inventing new type variable" messages.

Fix examples/l3-machine-code

stateLib.write_footprint was not working on the experimental kernel.

Improve stateLib.PC_CONV.

Works better with conditionals.

Update L3 examples.

Most changes relate to Poly/ML moving to fixed-width integers.

Opening lcsymtacs is no longer necessary.

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.

Towards decompilation of MIPS.

Fails for code with branches.

Contains minor changes elsewhere (e.g. handling of endianness and quotations).

Update ARM tools.

Provides support for a few more instructions.

Update for L3 examples.

Fixes a potential problem with the handling of word replicate.

Moves some shared code into stateLib (the register_combinations function).

Some other minor fixes.

Guard against some parsing problems.

Minor update to ARM tools.

word_memory_introduction now does a bit more simplification.

Refinement to stateLib.introduce_map_definition.

Should do a better job when simplifying reg-map updates.

Add tool support for working with ARM instructions MRS, MSR and RFE.

Fix for x86 decompilation with regards to jumps.

The x64_triples function was failing to generate two theorems and PC_CONV wasn't working for if-then-else terms.

Also support parsing of x86 condition pseudonyms, e.g. "jnae" (jump when not above or equal) is the same as "jc".

Patches following commit 0e49bf8.

The ARMv7 tools now support another memory representation.

Memory can now be treated as a map of type ``:word32 -> word32``.

Also reworked the tools with respect to the handling of word endianness.

Updates for machine-code tools.

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

Support for generating TEMPORAL triples.

Currently works for ARM, M0 and MIPS models. Yet to update the x86-64 model.

The ARM-M0 model is now hooked up to the "core/fast" decompiler.

Various updates/improvements to the decompiler tools.

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.

Update to stateLib.

Reorganisation of files under examples/l3-machine-code.