Don't export ERR from HolKernel

Move lambda type, dest_term function to kernel; add identical fn

dest_term is quite heavily used (it implements SML's best
approximation of a "view" for pattern-matching against terms), and its
implementation outside the kernel is needlessly inefficient.

Also extend signature with identical function, which correctly says
whether or not two terms are identical, including in their choice of
bound names. In the standard kernel, the possible presence of
explicit substitution terms means that this notion is not the same as
simple equality on terms.

Define sort_vars for use w/RESORT_{FORALL,EXISTS}_CONV

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.

Delete trailing whitespace in src/

generalising code of (l)_spine_binop to get strip_gen_left/right

Implement new, somewhat more generic subterm-finding functions.

These subsume my previous attempt in the same vein (bvk_find_term). In
this form, I believe gen_find_term will help with github issue #81,
which is to do matching-and-renaming on sub-terms, not just whole
goals or assumptions.

Minor simplification to find_term/find_terms.

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.

Move bvk_find_term (used in DEEP_INTROk_TAC) to HolKernel.

Document it and the other find_term functions from HolKernel.

Make new 'postkernel' directory to allow sharing of HolKernel module.

Intention is to move more code into this directory if it's possible to get
more sharing across the kernels.