Add some whitespace to signature files.

Floating-point update.

• isSignallingNan predicate is added to machine_ieeeTheory.
• The RISC-V model is simplified in places (for DIV and REM).
• The L3 import is extended to cover more operations.

Minor changes within floating-point theory.

• The operations float_negate1985 and float_abs1985 have been removed.
• Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan.
• Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.

Generalise some MIPS floating-point instructions.

The BC1* and C.cond.fmt instructions are no longer specialised to $fcc0 only.

Update MIPS tools to support floating-point operations.

This currently omits support for the floating-point memory operations, such as LDC1 and SDC1. (They should be straightforward to support.)

Remove some testing code.

Minor changes to printing of MIPS instructions.

Improve MIPS instruction parsing and printing.

Add MIPS floating-point instruction encoder.

Update MIPS model to include Mike Roe’s floating-point specification.

Also improve treatment of memory operations (so as to be more similar to the CHERI model).

Update for latest version of L3.

Update L3 examples.

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

Update SML files generated by L3.

The BitsN library has been sped up by removing word size checks.

Update MIPS model and tools.

The model now includes an instruction encoder.

Fixes for MIPS instruction parsing and encoding.

Update for L3 machine-code examples.

Some minor changes come from using the latest version of L3 when generating SML code.

The ARMv8 model gains a function for encoding instructions (in the logic). The step tools are updated to support the NOP instruction.

Update the MIPS example.

The model should detect more instances of branches in the branch delay slot, which is categorised as being unpredictable.

Add some assembly code support for the MIPS tools.