Ensure the bit-string rotate operations is well-defined on empty lists.
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.
The MIPS tools were experiencing problems with NOP instructions.

Reported by Brian Campbell.
Some fixes for the L3 ARM model.

A number of bugs were detected when validating the L3 model against the tests used to check the old (monadic) ARM model. These can be found here:

http://www.cl.cam.ac.uk/~mom22/arm-tests/

The bugs were as follows:

1. Off by one error in definition of SignExtendFrom.
2. Off by one error in definition of SignedSatQ.
3. Error in setting Q flag for QDADD.
4. Error in setting the GE flags for USAX and USUB16.
5. Error in the top-halfword result for SXTB16, UXTB16, SXTAB16 and UXTAB16.
6. Error in handling the C flag for some data-processing instructions (looks to affect immediate value variants only).
7. Incorrectly identifying some STRD instructions as unpredictable.

Note that 1-5 relate to instructions that are not supported by the decompiler, and 7 just prevented some valid code from being decompiled. As such, 6 is the most significant error fixed here.

The model now passes all of the tests.
Fixes for MIPS instruction parsing and encoding.
Add CHERI model under L3 examples.

CHERI is MIPS with capability extensions. See

http://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
Add support for MIPS instructions SC and SCD.
Fix optionSyntax.is_is_some
Merge pull request #213 from bacam/patch-1

Fix optionSyntax.is_is_some
add an experimental deep embedding of pattern matching

this is work in progress and far from finished
Expose conversion in x64_stepLib.
Remove HOL88-isms from FREEZE_THEN's doc-file.

Prompted by question from Rob Arthan on hol-info mailing list.
Changes to goal assumptions in FREEZE_THEN described more accurately
Remove calls to print_theory in enumfset/script files.

print_theory is fine to call interactively, but just adds verbiage
when done as part of a build.  Having done a build, looking at a
Theory.sig file is a good way to see what one has achieved.
Add tool support for the MIPS instructions LWL, LWR, LDL and LDR.
more work on deep-matches

- split pat and rh side of PMATCH_ROW
- this removes the need for higher order matching
- added guards to PMATCH_ROW
- add congruence rules for PMATCH
- work on parsing PMATCH
- work on using the simplifier with PMATCH
Merge pull request #210 from jeremydaw/trial

Implementation of the list_tactic concept.
Delete trailing whitespace in src/

This needs doing periodically, and is best done to a whole bunch of files
at once.