Update HolKernelDoc

Add sort_vars to HolKernelDoc

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.

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.

Add type definitions to HolKernelDoc.sig to make it compile with mosml.

Try to get HolKernelDoc.sig accepted by Mosml.

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.)

Have another go at getting HTML documentation working for HolKernel.