Update importer for latest version L3.

Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Support more than one method of detecting floating-point underflow.

Also update the L3 importer, which can be configured for different underflow detection options.

Update floating-point theory to specify exception flags for some operations.

• The flags are: DivideByZero, InvalidOp, Overflow, Precision and Underflow.
• The arithmetic operations now return a pair (flags and result).
• Native (oracle) evaluation has been overhauled. It now only applies to some 64-bit machine_ieeeTheory operations directly.
• The L3 Importer has been updated.

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.

Add facility for avoiding big record in L3 theories.

This can be invoked in L3 by calling `HolExport.bigRecords false`.

L3 no longer makes use of bit-vector modify.

Update L3 examples.

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

Update for latest version of L3.

Further support for L3 floating-point.

Update for latest version of L3.

Now supports floating-point square root and size conversions.

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.

Minor changes to L3 importer.

Update L3 import.

L3 now supports the list update operation.

Update for compatibility with the latest version of L3.

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.

The function Import.tDef now accepts a tactic (as well as a measure).

This allows L3 users to supply their own termination tactics.

Support for PAD_LEFT and PAD_RIGHT.

Fix in the printing of BFC and BFI instructions.

Similar to the previous commit.

Remove open_monad_syntax function.

Support more ARM VFP instructions.

Adds VMOV, VCMP and VMRS.

Update for L3 import (supporting more char/string operations).

Update L3 import files.

Automatically load monad syntax for monadic ARM (L3) model..

Updates to l3-machine-code.

Includes a monadic version of the ARM model, which includes data aborts.

Add some ARM VFP instruction support (under l3-machine-code).

New ARM and x86 instruction set models, with tool support for generating Hoare triples.

The new models are generated using a domain specific language; see ITP 2012 paper: "Directions in ISA Specification" (LNCS 7406).

The tools should be quite a bit faster than those found in examples/ARM/v7 and examples/machine-code. However, they are less extensive (this is work-in-progress).