Update for ARM-M0 model and tools.

The model inadvertently supported B.W instructions, which aren't found in M0.

Also fixes a problem with the evaluation of POP instructions.
Update for MIPS model and tools.

Simplifies handling of load/stores. (The tools now no longer attempt to accommodate reverse endian mode.)

Fixes modelling of exceptions occurring for an instruction in the branch delay slot. (This has to be properly processed and flagged using the component CP0.Cause.BD.)

Also fixed errors in the specifications of the MADD, MADDU, MSUB, MSUBU, SWR and SDR instructions. (Thanks to Mike Roe for testing the model.)
included missing open
Correct some documentation errors for various CHOOSE tactics.

Faults (to do with conditions on freshness of variables) identified by
Jeremy Dawson.
Correct bug in type pretty-printer when unary op is "unknown"

The buggy behaviour would cause

    minprint ``x: ('a -> 'b) option``

to print

    x: ('a -> 'b option$option)
Make type_pp a dependency for hol.bare's heap
Define OPTION_APPLY : ('a -> 'b) option -> 'a option -> 'b option

Give it <*> as syntax (following Haskell), as well as the 'name'
APPLICATIVE_FAPPLY, again from Haskell, where this operator is an
important part of the Applicative type-class (along with a "pure"
operator).
Get LIST_APPLY to use <*> syntax via APPLICATIVE_FAPPLY name.
minor tweak
Add assembly code parsing/printing support for the M0 and ARMv7 models.

There are new entry points to the decompiler. These take a function that maps a quotation (containing machine or assembly code) into a list of strings (typically hex). This facilitate the input of ARM assembly code. For example, the functions:

  m0_decompLib.m0_decompile_code
  m0_core_decompLib.m0_core_decompile_code
  arm_decompLib.arm_decompile_code
  arm_core_decompLib.arm_core_decompile_code

are provided with type

  : string -> string quotation -> Thm.thm * Thm.thm
definitions completed
Merge pull request #152 from domasin/master

definitions completed
Extend m0AssemblerLib and armAssemblerLib to include functions for instruction disassembly.

For example:

> print_m0_disassemble `f3ef 8100`;
mrs r1, apsr  ; f3ef 8100
val it = (): unit
Force --gcthreads=1 on poly invocations (in crudest way possible)

Closes #146
Share more code between mosml and poly Holmake.

Work on github issue #77
A new example demonstrating the zipper datatype (over lists)

Partly inspired by a challenge from Tony Morris
Allow prefix-operators to be printed without parens in rand-position

This is a refinement to the decision in aeb0085a3d11, which insisted
that prefix operators (like if-then-else, binders, case-expressions
and others) should always get parentheses when printed as arguments to
functions.

Now you can tweak this by choosing the NotEvenIfRand parenthesis style
as an argument to add_rule. For particularly tight operators, ones
that may omit spaces before their arguments say, this may look better.
For example, you might define a "#" operator, when it might be nicer
to have

  f #2 + g #n

print that way, rather than with extra parentheses. At the moment, our
standard number injection function & does print with parentheses, but
this case does feel like one where dispensing with the parentheses
might be a good idea.
Minor bug fix: ``&3:num`` should parse to a bare ``3:num``.

Otherwise, the result of parsing includes the unusable
``nat_elim__magic`` term.
Unicode emacs bindings; for \o{times,plus,slash,minus,dot} chars
Add binding for \sim character (U+223C ∼) to emacs unicode file.