Re-implement Datatype package with TypeBase sexps (not adjoin)

Fix ParseDatatype to handle recursive redefinitions

Implement most of a new Datatype function with nicer syntax.

(Pair-programming with Magnus who wanted it.) Still need to
implement change to EmitTeX.

Remove trailing whitespace in source files.

Cleaned up signature Datatype.sig. Added entrypoint
to call Hol_datatype on ParseDatatype.AST list input.

End of the *v saga. I found the spot in Pmatch.sml
that was failing to collect all the free vars
that needed to be renamed away from.

Misc. other tidying, including an incomplete
attempt at getting datatype constructors to
be defined in terms of numerals rather
than successors.

Liberate an AST interface to datatype declarations.

A slight extension to the way big records are handled, designed to give
users more control, and to also make the default behaviour more reluctant
to use big records (they can induce serious confusion if you're not
expecting them).

Modify TypeBases so that they can store conversions as well as theorems
in a tyinfo's "simpls_of" slot. This is then used to implement a conversion
for enumerated type equalities. Previously, we just used a rewrite
directly, which meant that something of the form (x = C10) might turn
into the rather ugly (foo_to_num x = 11). Now, the rewrite is only
applied to equalities between constants.
Some comments in the .sig files in Datatype, RecordType and EnumType
hopefully also make it clearer what the weird string results are
doing, and how they get added into theory files.

Moved the code to automatically generate "boolify" functions for datatypes
from src/datatype/Datatype.sml to src/Boolify/src/Boolify.sml.

It uses the register_update_function hook to add the boolification
info (more on that later).

Also added a test suite for boolification.

Minor inconsequential cosmetic changes made in the course of tracking
down various bugs.

Numerous small changes.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Idiotic hacking about to get aligned with EnumType.

Modifications caused by change of TypeBase signature.

New work aimed at making a single global EVAL function, with
an underlying compset.

Proper size definitions.

Modified to put size definitions correctly into the various tyinfos that
are generated, rather than defining the same set of constants once for
every type.

Changes due to the incorporation of John Harrison's datatype definition
package.
Here are the rest of the significant changes. The interface in Datatype
has been fleshed out quite a bit, but what was there has stayed pretty
much the same (except that prim_Hol_datatype doesn't write stuff out
to disk anymore; it's hardly very pure if it does so).

The ind_type theory is the basis for ind_types, which is in turn called
from Datatype.

Moved function for defining case constants over standard datatypes to
Prim_rec from Datatype.

Moved type_size and tysize to basicHol90/TypeBase. This lowers the
support required to apply these functions.

Initial revision