Remove eqtype declaration for term type

Minor tweaks to updateLib.

Improvements to updateLib. Added some comments describing the various conversions.

Note that the interface has changed a bit. Some conversions now take a compset (and/or a conversion) instead of a list of theorems.

Add conversion updateLib.UPDATE_APPLY_CONV.

Add some tools for working with function update (=+). The new directory
provides a suitable home for any future theorems/tools wrt =+.

To remove redundant updates you can do:

> OVERRIDE_UPDATES_CONV ``:num -> 'a`` [] ``(3 =+ a) o (4 =+ b) o (3 =+ a)``;
<<HOL message: inventing new type variable names: 'a>>
val it =
|- (3 =+ a) o (4 =+ b) o (3 =+ c) = (3 =+ a) o (4 =+ b):
thm

or

> OVERRIDE_UPDATES_CONV ``:num -> 'a`` [] ``(3 =+ a) ((4 =+ b) ((3 =+ c) f))``;
<<HOL message: inventing new type variable names: 'a>>
val it =
|- (3 =+ a) ((4 =+ b) ((3 =+ c) f)) = (3 =+ a) ((4 =+ b) f):
thm

This only works properly when you can evaluate equality on the update domain
(there are no free variables), i.e. here we know that 3 <> 4. The second
argument is a list of rewrites that can be used to evaluate this equality.

To sort updates you can do:

> SORT_NUM_UPDATES_CONV ``(4 =+ a) o (3 =+ b) o (2 =+ 1)``;
val it =
|- (4 =+ a) o (3 =+ b) o (2 =+ 1) = (2 =+ 1) o (3 =+ b) o (4 =+ a):
thm

This is a specialised version of SORT_UPDATES_MAPTO_CONV, i.e.
SORT_NUM_UPDATES_CONV is

SORT_UPDATES_MAPTO_CONV ``FST : num # 'a -> num`` numSyntax.less_tm []

The first argument maps the update pair (i.e. (l =+ r)) into some domain (over
which we do the sorting); the second argument is an ordering on that domain;
and the third argument is a list of evaluation rewrites.

Support is provided for sorting ``:'a word -> 'b`` and for ``:enum -> 'a`` for
some enumerated type, e.g.

> Hol_datatype `enum = One | Two | Three`;
<<HOL message: Defined type: "enum">>
val it = (): unit
> SORT_ENUM_UPDATES_CONV ``:enum`` ``(Two =+ a) o (One =+ b)``;
<<HOL message: inventing new type variable names: 'a>>
val it =
|- (Two =+ a) o (One =+ b) = (One =+ b) o (Two =+ a):
thm