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

Get irule (and IRULE_CANON) to do right thing with negated conclusions

Closes #775

Remove TABs in some source code, replacing them with spaces

Use Emacs's conception of how many spaces the TAB was
representing (and the M-x untabify command).

This may not line up with the author's original conception, but then,
using TABs makes it impossible to tell just what the original
conception was in the first place anyway.

Should probably script this over all of repository (excluding
makefiles of course), and use standard expand or col utilities rather
than emacs.

Remove eqtype declaration for term type

Drule.REORDER_ANTS_MOD, REORDER_ANTS, MODIFY_CONS

also arithmeticTheory.PRE_LESS_EQ

Delete trailing whitespace in src/

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

UNDISCH_SPLIT - undischarges antecedent and splits its conjuncts

Clean src/ to remove Unicode (or to mark it as OK)

Marking Unicode as OK is done by putting the UOK tag on the same line of
the relevant file.

PART_MATCH_A, REWR_CONV_A - allow substutiting in assumptions

define_new_type_bijections raises more info about how it was called

INST_TT_HYPS in Drule instead of Thm

reverting INST_TY_TERM to original version

this removes temporary code which tested INST_TT_HYPS every time
INST_TY_TERM was called

INST_TT_HYPS - as INST_TY_TERM but also retuns hyps in the order
they are returned by hyp (original theorem)

needed so that irule will give new subgoals in predictable order
temporary change to Drule.INST_TY_TERM is for testing

Tweak new code in Drule to avoid compiler warnings

Delete trailing whitespace in src/

docs for irule, prim_irule_tac, SPEC_UNDISCH_EXL

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

Tidy-up formatting of some src/1 code.

Tidy up some code under src/1. See commit ad9b041.

Remove trailing whitespace in source files.

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

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