Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Add QUIT_ON_FAILURE option and PAD_LEFT has moved from string to listTheory.

Change the specification wrt interrupt masking. The function arm_next no
longer masks interrupts -- this is instead left to the level above,
e.g. arm_run.

Other changes include more checking of step theorems in selftest. Also made use
of tools in updateLib.

Minor change capturing unpredictable case for LDM -- from latest ARM reference
errata 7.

Changed the return type for functions provided by arm_parserLib and
arm_encoderLib. They now include a symbol table, which identifies the address
of labels.

Clean up following changes to EmitML. Also, some other tweaks wrt evaluation.

Update that adds support for ThumbEE.

/* From the ARM reference...

ThumbEE

Is a variant of the Thumb instruction set that is designed as a target for
dynamically generated code. It is:
* a required extension to the ARMv7-A profile
* an optional extension to the ARMv7-R profile. */

Added support for hardware interrupts: reset, fiq and irq. This adds an extra
argument to the next state functions, i.e. we now have

arm_next : iiid -> HWInterrupt -> unit M

and

ARM_NEXT : HWInterrupt -> arm_state -> arm_state option

In the absence of an interrupt, the previous behaviour is obtained with

ARM_NEXT NoInterrupt : arm_state -> arm_state option

The single-step behaviour for interrupts can be obtained with

armLib.arm_step "" "reset" (* ARM_NEXT HW_Reset *)
armLib.arm_step "" "irq" (* ARM_NEXT HW_Irq *)
armLib.arm_step "" "fiq" (* ARM_NEXT HW_Fiq *)

There has also been some minor tidying-up to the code.

Tweak definition of encode_psr and remove some unused code.

A few changes:

1. Make it clear that the ARMv7-M profile is not properly supported (yet).
2. Fix for EmitML script (following changes to memory).
3. Fixed parsing/encoding for 16-bit Thumb MOV (register) instruction.
4. Fixed bugs in model for BFI, SSAT and SSAT16.

A new Monadic ARM instruction set specification. Covers all current ISA
versions i.e. ARMv4 to ARMv7.

Doesn't cover the ThumbEE, VFP and Advanced SIMD extensions. Also doesn't
model hardware interrupts - these will be added at a later date.

To use the armLib tools, Moscow ML users will likely have to apply the patch to
avoid the Chr exception.
<http://hol.sourceforge.net/mosml-chr-instructions.html>