Promote (SML) $ to Lib; update its fixity; document it

Allow Induct_on & Cases_on to use different theorems with 'using'

The using function is infix on tactics; other tactics can grab 'using'
theorems if they want to try, using the markerLib.maybe_using
entrypoint.

Implement -*, an operator to remove stuff from simpsets

It takes a list (hence the '*') of strings naming conversions or
rewrite theorems and removes them from the simpset.

The tracing machinery is also adjusted to make rewrites better
identify the theorem that is being used.

Fix use of Thm sigs to let logging kernel's extended version be seen

Now the theorem implementations don't refer to the theorem signature;
the binding and hiding happens in Overlay.sml.

Really remove "eqtype-ness" from terms

At some stage on this branch my messing with Overlay and similar
things allowed the representation of terms as an equality type to
sneak through, at least under the standard kernel.

Promote more functions from Isabelle Library into Portable

- enclose l r mid is "just" an application of string concatenation,
but is useful when partially applied to two arguments
- filter_out is filter with the sense of the predicate flipped
- ? provides a compact way of writing "if b then f x else x"

Finally, move fold_product from Library to Graph, where it is used.
This library function is effectively a fold over a cross product of
two lists + an accumulator. It's nice not to have to compute the
cross product explicitly, but it's a bit too exotic for me. I grepped
for uses of it in the Isabelle sources, and even there it's used only
6 times.

Add "flipped" versions of apfst, apsnd and uncurry (from Isabelle)

These are "flipped" infixes just as |> is a flipped application
operator.

Thus

pair |>> f

is the same as

apfst f pair

||> is apsnd, and ||-> is uncurry. The latter has definition

fun (x,y) ||-> f = f x y

This is a prelude to better incorporation of the concurrent futures
implementation currently stashed in portableML/poly/fromIsabelle,
which is in turn work towards github issue #575.

Move smpp to Portable - get everything up to arithmeticScript working

Updated as far as type_grammar.sml

Work towards use of PolyML.pretty type for most pretty-printing

Compiles up to src/parse under Poly/ML

Standard and experimental kernels now share Thm.sml implementation

It should now be possible to have the logging kernel work over either
implementation of terms, and to delete its copy of Type, Term etc.