Fix typo in hol-unicode.el
Make dependencies in src/num/arith/src's Holmakefile more accurate.
Delete generated file (src/string/theorytesting/stringlit_output)
Delete a munger.o file by listing in an EXTRA_CLEANS
Remove -small option to build.

It didn't work at all under Poly/ML and caused problems with Moscow ML
as well.  I suspect no-one ever used it.  Closes #184
Git-Ignore generated file in src/string/theorytesting
Make Poly Holmake retain intermediate files when it fails in debug
mode

In particular, it can be useful to look at the list of dependencies
and the executable when things go strangely wrong.  These files were
being deleted too eagerly.
Handle corrupt Systeml.sig when moving build from Moscow ML to Poly.

This is analogous to what was done in b151b8f0 (Jul 2009), which coped
with building a Moscow ML setup on top of a build that used to be
Poly. There the claim was made that the reverse situation (the one
fixed in this commit) didn't need anything done to it. That was
because poly's Systeml.ui was being generated afresh with every
configure, right up until 331d321e (Jan 2014).
Merge pull request #183 from ptroja/master

Minor fixes to "DESCRIPTION" manual
Revert 'Consistent use of "failure" instead of "failure occurs".'

This reverts commit 15eb27acf8aacdea8d4e9a4c92c49d93e372f6bf.

"Failure occurs if ..." is more grammatical than "Failure if ...".
There are some existing occurrences of the latter that still need to
be fixed.
Fix some unnecessarily terse "Failure if <some condition>" clauses

Better is "Failure occurs if <some condition>". Such sentences have
verbs.
Clean up some doubly-nested LaTeX environments for the sake of Emacs.

The problem is not the double-nesting per se, but the use of

    \begin{foo}\begin{bar}
    ...
    \end{bar}\end{foo}

which, when bar is "alltt" or "verbatim" seems to cause AucTeX to get
into a terrible font-locking confusion.

Also remove some unnecessary local definitions of \bk to be a teletype
backslash when our commands.tex include-file has \bs for this
character already.
Implement and document a new prove_case_rand_thm function in Prim_rec.

This will be the basis for a general tool that moves case-constants up
within a term and then eliminates them, subsuming, for example, the
functionality in boolSimps.COND_elim_ss, which does this but only for
the boolean case-constant (aka if-then-else).
Fix order of the existentially quantified vars in list_nchotomy thm.

This makes the theorem conform to the pattern used by types in the
TypeBase. This theorem is stated explicitly here to override the
datatype package's choice of variable names, which make a difference
when you use Cases_on or Cases.
Implement function to prove a case-constant elimination rewrite
Remove two uses of old if-then-else syntax from the REFERENCE
Fix quantHeuristics selftest to cope with change in cd00950
Typography: extra space caused by \index{...} \index{...} removed.