Remove unnecessary KernelTypes.sig in src/0

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.

Constants are no longer considered out of date if their witnesses
become out of date. Thus, one might define
c = rhs
and save this definition with name "c_def". Subsequently, if
something in rhs becomes out-of-date, then c_def will be removed from
the theory. However, this change means that the constant c will
remain, as will any theorems mentioning it and not otherwise
out-of-date.

Next change in this area will be to attempt to share Sig or something
like it between both kernels.

Move the implementation of Tag.sml from src/0 into src/prekernel so that
the standard and experimental kernels can share it. Also make the
experimental kernel restrict the Tag interface in line with what the standard
kernel does. Implement this restriction slightly differently in the
standard kernel in terms of files and their names: make the unrestricted
implementation a normal mosml module (Tag.sml and Tag.ui), and then later
restrict by applying a separately ("toplevel") compiled signature. This
approach seems to require less complicated makefiles.

Fix for soundness bug; Globals.old changes its behaviour, and is no longer
a reference. It is used in the kernel to do semantically significant things
so can't just be left to a user to change arbitrarily.

minor additions and alterations.

Fairly radical changes: theorems' hypotheses now stored in a binary tree.

Instituting paired syntax. Long live paired syntax!

New Kananaskis kernel.