Make REWR_CONV report bad rewrites in ASCII

This would be better still as a term argument to the HOL_ERR (see #622).

Tidy up copyright documentation

- Move some information out of file headers into various files in
doc/copyrights.
- Reinstate a LICENSE file for examples/muddy (which is LGPL).
- Identify code taken directly from Poly/ML implementation in
tools-poly/holrepl.ML

See github discussion at

https://github.com/HOL-Theorem-Prover/HOL/issues/559

for more on this.

Closes #559

Delete unnecessary code in Conv.testconv

Handling an exception only to reraise it is a no-op (brain fart
introduced by me in ea1b9b0f59).

Define an exception-tracking wrapper function w in Conv.sml

Indicative uses (around CHANGED_CONV, SKOLEM_CONV and X_SKOLEM_CONV)
are commented out.

Use new Portable.reraise in Conv.testconv

Add “SPLICE_CONJ_CONV”; add tacticals “wlog_tac” and “wlog_then”.

Tail-recursive “REPEATC”.

Remove eqtype declaration for term type

Fix EVERY_CONJ_CONV; add tests for EVERY_DISJ_CONV

Add IFC, an if-like construct for conversions

(With Michael.)

Also, use it to re-implement REPEATC, removing an unnecessary handler
(in ORELSEC).

Add Conv.memoize.

This can be used to build conversions that lookup previous result in a red-black tree.

The n-bit libraries are updated to make use of Conv.memoize and new functions in computeLib.

Delete trailing whitespace in src/

HYP_CONV_RULE - apply a conversion to hypotheses of a theorem

PART_MATCH_A, REWR_CONV_A - allow substutiting in assumptions

Implement HOL Light's {PAT,PATH}_CONV.

Closes #255

Add COMB2_CONV to Conv structure.

This is an import from HOL Light, changed only to handle the UNCHANGED
exception appropriately.

In passing, update COMB_CONV documentation to
* mention COMB2_CONV as a see also;
* close a parenthesised aside;
* describe its behaviour in the face of UNCHANGED

Fix minor bug in behaviour of EVERY_CONJ_CONV (with selftest)

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

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