Merge pull request #185 from ptroja/master

Removing extra space in DESCRIPTION manual
Remove broken and unnecessary {temp_,}add_binder entry-points in Parse
Fix for MIPS SUBU instruction.
ARMv8 model and tools.

This model supports AArch64 mode only, i.e. there's no support for the AArch32 mode.
New theorems about finite maps and alists

Importing theorems that were useful in CakeML (https://cakeml.org).
Mostly by Ramana Kumar, some by Scott Owens.

Also removed the unnecessary ALL_DISTINCE assumption from
ALOOKUP_TABULATE.
A few set lemmas from CakeML.
Added CakeML list theorems to listScript.sml

Added a new function, nub, which removes all duplicates.

I'm not sure how to decide what goes in list and in rich_list, so I put
everything in list that I could. That is, everything but theorems about
rich_list only constants and theorems whose proofs depend on rich_list
theorems.
More CakeML theorems about lists

The ones that couldn't go into listTheory
move theorems out of finite_mapTheory into (rich)_listTheory

they have nothing to do with finite maps
store map_replicate in rich_listScript.sml

rather than proving it and throwing it away
Added lemma about going in MAX_SET
Improve nub_set lemma

As suggested by Michael Norrish
Two more lemmas about lists from CakeML
A few theorems about sorting and permutations
Add sorting/perm theorems to finite_maps and alists

This makes the finite_map directory depend on the sorting directory.
Document 'nub'
Fix examples/parsing/NTproperties in light of 932238d

Issue in latter commit is its introduction of theorem FLAT_EQ_NIL,
which overrode my own local theorem of the same name. Fixing the order
of the open declarations fixes this, but I also simplified a couple of
proofs slightly along the way.
Use [simp] rather than export_rewrites in a few places.
A new test-case for pretty-printing field selections to TeX
Define \HOLFieldName macro rather than \HOLFldName

Bug spotted by Ramana.