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

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.

documentation for HYP_CONV_RULE, UNDISCH_SPLIT

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

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