Minor updates to L3 ARM models.

Update ARM-M0 model for latest version of L3.

Update the ARMv7, ARM-M0, MIPS and x86-64 models.

Exported from the latest version of L3.

Update for the latest version of L3.

Changes have been made when exporting operations of the form:

`f : args -> state -> value * state`

If the state is not changed then this is now exported as

`f : args -> state -> value`

If the state is changed but the `value` type is `unit` then it this is now exported as

`f : args -> state -> state`.

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.

Update for the latest version of L3, which has additional floating-point support.

Cover IEEE754:1985 behaviour for "abs" and "neg". Also adds support for "compare", "toInt" and "fromInt" at the machine level.

Update model for latest version of L3.

Update for ARM-M0 model and tools.

The model inadvertently supported B.W instructions, which aren't found in M0.

Also fixes a problem with the evaluation of POP instructions.

Fix a couple of minor glitches in M0 model/tools.

Reported by Brian Campbell.

Update ISA models.

The new models are generated by the latest version of L3. This mostly results in just a few formatting (pretty-printing) changes. However, bit-patterns are now expanded out in a different manner. Specifically, applications of “word_extract” (over the match word) are replaced with applications of “v2w” (over the bits generated by “boolify”). Some minor updates were needed to accommodate this change.

Minor change to ISA models.

All ‘rst record fields are now prefixed by the type name.

Support a few more M0 instruction instances.

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.

Some minor formatting (printing) changes in the L3 instruction set models.

Minor tweak to M0 decoder.

Add ARM-M0 model (and tools) to examples.