Add some test-cases for simpset-recreation entrypoint

Fix a bug and add some tests

Add a new set of "global simplification" tactics

(Thanks to James Shaker for the suggested name.)

The "global" means that these simplify every assumption with respect
to every other assumption before eventually simplifying the goal as
well.

The core primitive is in simpLib and takes a simpset and a
configuration record as a parameter. The bossLib variants use letters
in the name to encode the common configuration options, and always use
the standard simp/fs/rw stateful simpset. These are gs, gvs, gns and gnvs.

The addition of the 'n' and the 'v' toggle independent behaviours:

'n' - don't use 'strip_assume_tac', meaning that goals won't
strip. (Existential variables won't get chosen and conjuncts
won't strip either; I may go back on both of these.)
'v' - eliminate variables (like VAR_EQ_TAC)

I hope that gs (or gvs) will replace the need to do the

fs[] >> rfs[] >> rveq >> fs[]

"dance" in complicated proofs with big assumption lists.

Make resolve_then try harder to keep assumptions "in order"

In particular, when resolving p1 ... pn ==> qj against q1 ... qm ==> r
the result will be

p1 ... pn q1 ... q{j-1} q{j+1}...q{m} ==> r

modulo the fact that unification may cause assumptions to become the
same (duplicates are eliminated), either as each other, or as an
existing hypothesis. This makes the proposed irule (goal_assum o
resolve_then Any mp_tac) behave a bit more like MATCH_MP_TAC, rather
than as currently.

Ensure ℕ and ℝ dp's have different names when embedded in simplifier

Now they are NUM_ARITH_DP and REAL_ARITH_DP, which are the names to
use when "Excl"-uding them from simplifier invocations. The
NUM_ARITH_DP also does normalisation over additive ℕ-terms.

Fix a test-case broken by strengthened simplifier

Make Excl also filter out d.ps with given name

Provide new term-based version of Cases_on

This version takes an extra string list parameter for specifying names
to be used in the split.

Test-case demonstrating TFL extracting bad termination conditions

Though the first definition made looks reasonable, it is still not
quite right: it should refer to an _aux constant in the nested
recursion case, and doesn't.

More fixes given testutils API change

Add regression tests for find_consts

Revise the way "exclusion/deletion" strings are handled by simpLib

The srw_ss() simpset includes the list.APPEND_ASSOC rewrite, and this
new method allows for the strings "APPEND_ASSOC" and
"list.APPEND_ASSOC" to remove that rewrite. Importantly, the former
will hit other theorems of that name from other theories (though I
admit that's yet to be part of a regression test).

Control generation (and storage) of TypeBase simpls fields better

Core types were picking up extra copies of their simplification fields
and more was being written to disk than necessary.

With test cases

Remove eqtype declaration for term type

Rename match_all_tac to first_match_tac

The new name is less confusing, given what it does.
Arguably it does not need to be bound at all, since the implementation
is so simple.

Make match_goal tests use OK(); not print "OK\n"

Fix many selftests to have prettier output

Move match_goal selftests to boss

Enables writing tests depending on more stuff (including BasicProvers).

Add (currently failing) test for qhdtm_x_assum

MATCH_ABBREV tactics now ignore _ in patterns

Tactics affected are
- MATCH_ABBREV_TAC
- HO_MATCH_ABBREV_TAC
- MATCH_ASSUM_ABBREV_TAC

Documented and self-tested

Document new_type_definition's errors better; improve its error-reporting

Closes #128

Test and fix for omissions in computeLib’s handling of sums.

New regression tests for EVAL (focusing on case-constants of course).

Move selftest to datatype directory, where it more rightfully belongs,
and incorporate some new tests from the ParseDatatype.sml file. (These
needed updating because they weren't themselves valid.)

More regression tests. I believe all of the included calls to
Hol_datatype should work.