align numeric syntax: 'great' becomes 'greater' The earlier names are inconsistent with numSyntax and less descriptive.

The changes are:
intSyntax.great_tm -> intSyntax.greater_tm
intSyntax.dest_great -> intSyntax.dest_greater
intSyntax.mk_great -> intSyntax.mk_greater

int_arithTheory.add_to_great -> int_arithTheory.add_to_greater

realSyntax.great_tm -> realSyntax.greater_tm
realSyntax.dest_great -> realSyntax.dest_greater
realSyntax.mk_great -> realSyntax.mk_greater

github issue #629

Complete purge of references to Datatype.big_record_size

Left over from 3383b4b950

Tweaks (and some temp debug code)

Remove Globals.priming.

Also remove references to it in code that isn't being tested in the
regression checking build-sequence, and so is probably bit-rotted.

Provide numvariant version of variant, which behaves like

with_flag(Globals.priming,SOME "") (variant avoids)

Document change/incompatibility in release notes.

Fix examples/l3-machine-code

Update importer for latest version L3.

Remove eqtype declaration for term type

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`.

Avoid calling Theory.{new,export}_theory directly in L3 Import

By calling the versions in HolKernel instead, we enable automated
proof-recording for OpenTheory more easily.

L3 no longer makes use of bit-vector modify.

Make more of the floating-point library available to Moscow ML users.

Evaluation now works under Poly/ML. However, Poly/ML is needed for evaluation
using native floats (which is controlled through the "native ieee" trace).

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.

Avoid "inventing new type variable" messages when loading Import.

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

Minor changes to L3 importer.

Update L3 import.

L3 now supports the list update operation.

Update the MIPS example.

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

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.

Update L3 import.

Extra bit-string shifts are supported.

Add a bit-string rotate operation.

L3 now supports type conversions for char.

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

This allows L3 users to supply their own termination tactics.

Update L3 import.

Reverse can now operate over lists (and strings).

Support for PAD_LEFT and PAD_RIGHT.

Fix in the printing of BFC and BFI instructions.

Similar to the previous commit.

Minor update to Import code.

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..

Move bitTheory into src/num/extra_theories and move evaluations theorems in wordsLib further up the build sequence.

Includes some tidying-up work.

This closes issue #120. Evaluation for "toNum" and "toString" can now be enabled by loading up stringLib (or, more precisely, ASCIInumbersLib), without the need to load up wordsLib.

This check-in can be viewed as finishing off the (many) loose ends left over from work on issue #70.

Updates to l3-machine-code.

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

Minor tweaks for l3-machine-code example.

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

execute several heuristics for pattern-matching and choose the best result
interface of pattern matching simplified

adaption to changed interface of pattern-matching

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).