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

Update the ARMv8 model and tools.

Some basic functions have been inlined.

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.

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.

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

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.

Update ARMv8 model.

The encoder now explicitly defines an encoding function for bit-mask values. This avoids the use of a reverse look up function (implemented with sptress). Thanks to Shaked Flur for implementing the encoding algorithm.

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 for ARMv8 model and tools.

Contains some fixes for the decoder.

There is now support for assemble code syntax.

Add support for the ARMv8 instruction CCMP (register).

This instruction was inadvertently left out (only the immediate variant was modelled). A few minor changes are made elsewhere.

ARMv8 model and tools.

This model supports AArch64 mode only, i.e. there's no support for the AArch32 mode.