Move the match_position datatype from mp_then to its own file

This type will be used in the API to the forthcoming resolve_then.
Separating it out into a _dtype.sml file also avoids having to repeat
the datatype definition in .sig and .sml file.

Move mp_then.PART_MATCH' to Drule and document it

Make mp_then(thus drule*) GEN_ALL on implicational theorem as step 1

Provide mp_then with a signature

The documentation for mp_then does not appear in the auto-generated
HTML index. This seems to be because it has no signature. This adds
a signature for mp_then so that it becomes visible in the generated
HTML index.

mp_then: Make Pat selector backtrack over possible parses

With regression test.

Closes #567

Fix an mp_then/Pat selector bug

Include some more selftests. Thanks to Ramana for the bug report.

Fixes for mp_then/drule bug found in previous commit

Provide more test-cases as well. Extend normalisation done by
goal_assum after a theorem is returned to it after "resolution".

Fix mp_then bug: its PART_MATCH variant wasn't instantiating types

(It has a PART_MATCH variant in order to make sure preserve universal
quantification of variables that don't get specialised to make the
match happen.)

Remove eqtype declaration for term type

Fix over-aggressive normalisation in goal_assum

In particular, it's important that

P1 /\ P2 /\ ... Pn ==> F

stays as an implication and not turned into a negation.

Add test for expected behaviour with some instantiation provided by
mp_then.

Improve mp_then to eliminate matched preconditions

Make mp_then compile under Moscow ML

Write general imp_res_tac-like tool for combining thms