Repairs to ARM/v7/eval.

This was affected by the reordering of arguments in case constants.

The script files in src/emit have been restructured into two theories: basis_emit and extended_emit.

This will break uses of EmitML, but these can be easily fixed — see examples/ARM/v4/arm_emitScript.sml and examples/ARM/v7/eval/arm_emitScript.sml.

More removal of old-style case expression syntax.

sign_extend has moved to wordsTheory. Also, avoid TeX_notation warning.

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

Fixes for EmitML script.

Also, get RFE instructions working (albeit very slowly) with arm_step.

Refinements to the ground-term evaluator. To simplify things, the function
update (=+) sorting conversion has been removed. Instead updates are sorted
just prior to printing.

The elf object file loader now includes the "data" and "rodata" sections.

Poly/ML users can now build a stand-alone ARM assembler by using the code at
the end of arm_evalLib.sml.

add_with_carry has moved to wordsTheory. Also made some tweaks to evaluation.

Support for ground-term evaluation of the ARM model within HOL -- the program
memory is implemented as a Patricia tree.