Fix examples/l3-machine-code/m0 for tight equality

Remove eqtype declaration for term type

Fix m0_step for length-nil #346

Update ARM-M0 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.

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

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.

Avoid an unnecessary Alignment condition appearing in the ARM-M0 triples for LoadLiteral instructions.

Remove occurrences of testbit from ARM-M0 triples.

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

Reported by Brian Campbell.

Fix for M0 tools with regard to POP (with pc) and PUSH (with lr) instructions.

The fix ensures that SEP_ARRAY introduction works for these instructions.

Updates for machine-code tools.

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

Tool support for "LDR (literal)" under M0.

Support for generating TEMPORAL triples.

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

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.

Support a few more M0 instruction instances.

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