Move some of the machinery behind BasicProvers.VAR_EQ_TAC to Tactic

Move some term-equality helper functions from boolLib to boolSyntax

This helps with dependency chains and provides some documentation in
that they now appear in a signature file for the first time.

Update src for strip_binop change

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

Document them in .doc files

Add type unification and mk_ucomb to boolSyntax

Add syntax/ops to make set manipulations easier

Remove small instance of some unused code

Remove redundant add_type calls

boolSyntax.new_type_definition called add_type after a type was defined,
even though the hook machinery now takes care of this.

In boolScript, there was a similarly unnecessary call to add_type after
the itself type operator was defined.

Make new_definition_hook replace a constant on the LHS by a variable

new_definition calls gen_prim_specification which requires an equation
whose left-hand side is a variable, but sometimes (maybe only in obscure
old example script files) users pass an equation with a constant on the
left. The same hook that abstracts arguments now turns a constant on the
left into a variable.

Start of project to flip argument order in case constants.

One scary (but probably optional) change is to do away with bool_case
constant because it is now identical to COND. This could be reversed,
but having two constants with exactly the same type and semantics does
seem silly. I think the parsing/pretty-printing behaviour can be made
sensible even in the face of this unification.

Prim_rec’s functions for defining case constants and proving case
congruence theorems have been adjusted appropriately.

This is relevant to Github issue #97.

Put some syntax operations for bool$IN into boolSyntax.

Add extra term/syntax functions to HolKernel. Also tweak definition of HolKernel.find_terms.

The new definition of find_terms may or may not be quicker.

The new functions are:

list_mk_icomb (a type instantiating version of list_mk_comb)
mk_monop (this is essentially a curried version of boolSyntax.mk_icomb)
mk_binop
mk_triop
mk_quadop
syntax_fns (This is taken from bitSyntax and provides a quick way to define syntax functions. Designed to work with the "mk" functions above.)

More theory signature events now reported to hooks.

In particular, {new,remove}{typeOp,constant} events are reported.

Use this to do away with some of the cruftiness in boolLib whereby the
entry-points there had to mask the primitive principles in order to
update the grammar. Now the parser installs hooks to watch for things
being deleted or added and adjusts the grammar as it goes.

The disadvantage is that it's impossible to bypass these changes to
the grammar.

Tidy-up formatting of some src/1 code.

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