Improve TypeBase API for reporting on record fields

Datatype code now bypasses treatment of "big records". This stuff can
all be deleted and I will be happy to see it go as it is horrifically
complicated, and usually only serves to confuse users.

Thanks to a CakeML Slack discussion for the push to make the API
change.

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

Ensure record type constructor names don't interfere with user names.

When you declare a type like

foo = <| n : num ; b : bool |>

there is an underlying constructor defined called foo:

foo : num -> bool -> foo

This underpins the definition of the various functions over record
types, which are made with the recursion principle for this underlying
algebraic type. However, with sufficient care/malice, this constant
(which users are typically oblivious to), can interfere with other
definitions to ill effect.

The fix is to make the constant take a name that can't even be
generated by the parser, but to then overload the name ("foo" in the
example) to this constant. The parser is happy to have a string
overload to multiple constants; the internal theory signature
mechanism has to prevent multiple constants from having the real name.
(Before the fix, the kernel signature maintenance lets the second
definition of a constant with this name go through but invalidates the
first constant, causing a theory to purge itself of what the user
thinks is a perfectly valid type.)

This solves one of the problems identified in github issue #224.

trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

The new changes to records have been fixed so that the system
will rebuild without error. Whether the record stuff actually
does what it should, I am still checking. The big record
stuff will have to be checked in Australia, probably, since
I don't really understand it.

Fixes to support code generation for records. Incomplete! So
do not update these changes (I'm just using CVS to transfer
files to work machine).

A load of changes aimed at supporting records better. And some other
odds and ends.

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.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Modifications caused by change of TypeBase signature.

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

Changes due to the incorporation of John Harrison's datatype definition
package.
In particular, record type definition is now done elsewhere, code here
just takes a tyinfo and proves all of the extra theorems (including some
definitions) appropriate for a record type.

Fairly wide-ranging modifications to make Hol_datatype take record type
definition quotations as well as normal types. The syntax supported is:
tyname = <| fld1 : ty1 ; fld2 : ty2 ; fld3 : ty3 ... |>
Not extensively tested.

Initial revision