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.

Improve the interface to stateLib.update_frame_state_thm.

Also add some explanatory comments within stateScript.sml.

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.

Minor update to ARM tools.

word_memory_introduction now does a bit more simplification.

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

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.

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.

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