Fix l3-machine-code/arm for tight equality

Reconcile store_thms with diverging names in db and val binding

Remove eqtype declaration for term type

Add arm_stepLib tool support for some SUBS PC instructions.

These instructions are used for exception return.

Fix arm_step for length-nil

c.f. f999459ad3f740e556b2302feb10a24c69d24222

This shows up that these theories aren't in the build sequence.

Improve handling of BitFieldClearOrInsert instructions.

Update ARMv7 model for 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`.

Update L3 examples.

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

Opening lcsymtacs is no longer necessary.

When casting from a bool to a bit-vector use "v2w" instead of a conditional expression.

Make use of alignmentTheory in the l3-machine-code examples.

Towards decompilation of MIPS.

Fails for code with branches.

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

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.

Update ARM tools to eliminate occurrences of the bitstring operation testbit.

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.

Updates for machine-code tools.

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

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.

Update to ARM tools.

Triples are now generated with a "mode" variable. This is required to satisfy the "GoodMode" predicate. Before concrete modes were used, e.g. "16" for user mode.

In addition, various performance related enhancements have been made in helperLib (especially with regard to AC rewriting for the "*" operator).

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 more ARM VFP instructions.

Adds VMOV, VCMP and VMRS.

Missing files from last commit.