Implement some new derived rules for manipulating implicational thms

The pp rule allows for transformations akin to what happens as part
of the action of mp_then. The iffLR, iffRL and cj functions allow
useful manipulations to happen under universal quantifiers and
"preconditions". Documented but without regression tests.

Move mp_then.PART_MATCH' to Drule and document it

Move some unification related functions out of transfer into src/1

Document them in .doc files

Various doc fixes

Drule.REORDER_ANTS_MOD, REORDER_ANTS, MODIFY_CONS

also arithmeticTheory.PRE_LESS_EQ

Expose and document IRULE_CANON.

This function is similar to MP_CANON (which is undocumented), and
normalises theorems to make them usable as introduction rules (as is
done by the irule tactic). Also tweak irule's documentation to better
reflect this implementation.

Finally, give irule an alias in Tactic as IRULE_TAC.

documentation for HYP_CONV_RULE, UNDISCH_SPLIT

PART_MATCH_A, REWR_CONV_A - allow substutiting in assumptions

INST_TT_HYPS in Drule instead of Thm

Tactic.irule, also prim_irule_tac and Drule.SPEC_UNDISCH_EXL

Drule.ASSUME_CONJS

Constructs a theorem proving a conjunction from its individual conjuncts

Drule.EXISTS_LEFT, Drule.EXISTS_LEFT1 added

to existentially quantify hypotheses in a theorem

UNDISCH_TM, which also returns the term made an assumption

Change src/bool to src/1 as a prelude to experimentation!