extra semicolons removed from (some) .sig files

Made the interface to OmegaMLShadow sufficiently general that it can be
run as ML code without any recourse to the HOL kernel. (The basic change
is to make the data type representing proofs not necessarily have terms
at its leaves, and to instead have alphas.)

Gave this module a signature file, with documentation, and also fixed a
bug found by Mike; OmegaSimple was making the classic mistake of using
the global grammar to do its parsing.