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.
Extend simplifier's treatment of abbrevs to handle abstractions better
Trailing-whitespace deletion script now handles tabs also

There is also a -n option to see what it might affect without actually
going through with the replacement.
Fix error in prtermScript caused by abbrev change (e693dc9).
Update L3 import.

Reverse can now operate over lists (and strings).
Fix for x86 decoding of instructions with a SIB byte when there is no base register.

Need to read a 32-bit displacement in these cases.
Mention list range theory in release notes.
Define MAX_SET on the empty set to equal 0.

This make the relevant equation

    FINITE s ==> (MAX_SET (e INSERT s) = MAX e (MAX_SET s))
Fix a couple of proofs broken by change to MAX_SET definition.
The function Import.tDef now accepts a tactic (as well as a measure).

This allows L3 users to supply their own termination tactics.
Update Nat functions for parsing numbers from strings.

They should now return NONE in cases where they would previously raise an exception.
Minor tweaks to comments.