extra semicolons removed from (some) .sig files

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

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

BIG refactor: mainly to allow stdknl to use SharingTables technology.

SharingTables implements hash-consing for types as they are written
out to disk. This can make a big difference to the theory file size,
and thus to theory-loading times.

The big visible change is that Theory, TheoryPP and Definition are no
longer really part of the kernel, and are found in src/postkernel
instead. They don't need to know about secret implementation details
in terms, types or theorems. They do need to have access to

Term.{write,read}_raw

and primitive definition principles (which are in Thm).

Another API change is that Tags no longer use user-visible string refs
to record use of axioms. Instead, the refs are hidden behind a new
Nonce type. This in turn means that the Tag.axioms_of function can
move to be visible to all users after the kernel. (If we kept the
axioms as string refs, users could alter the strings being pointed
to.)

Forgot to include the new functions in the 0-kernel signature files.
Also, fix for the Makefile to make it see a dependency.

Rework a bunch of code in the two kernels so that they can share even
more stuff in src/prekernel. In particular, the latter is now home to
a special purpose symbol table that knows all about things being
up-to-date. Also move the final signatures for Terms and Types that
are what is ultimately presented to the user into prekernel so that
both kernels can use them.
In src/0 also move the signatures in Raw-sig into Type.sig and
Term.sig so that {Type,Term}.sml can be compiled in normal mode
against those signatures. I think this makes things a deal cleaner
there.
Finally, witnesses have entirely disappeared from src/0. If we
wanted to reinstate them for whatever reason, they could be stored in
a KernelSig.symbol_table along with arities and base types.

New Kananaskis kernel.

Deletion of "dummy" type. No longer needed because of MN's new
type inference implementation.

Removed references (Link and Stv constructors) as type unification is now
done at the level of the TCPretype in the parse directory. This simplifies
the implementation considerably.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision