Fix code to work under Moscow ML

Put application of functor Graph into separate file to create
SymGraph, a Graph where the node keys are "syms" (aka strings). This
is by analogy by the way Symtab is defined.

Implement s-expression type for use in serialisation applications

Improve Moscow ML's handling of holpathdb

Thanks to Chun Tian for the bug report.

Closes #737

Promote Isabelle's Graph functor to src/portableML

Lift Table functor out of fromIsabelle into src/portableML

This code is Isabelle's workhorse version of our Binarymap. It has a
better API for working with maps into lists of values, and is also
better in that its use of a functor means that the types of
maps/dictionaries/tables using different comparison functions are
different.

I have altered it to use HOL style comparison functions that are
curried rather than tupled. (I.e., in Isabelle the equivalents of our
various op_<operation> functions are take a comparison function that
takes a pair of arguments; our tradition is to use a curried
function.)

I have also added pretty-printing, requiring KEY-structures to provide
a pp function. (These functions ignore depth arguments for the
moment.)

Finally, there are a number of knock-on effects in the fromIsabelle
directory.

mosml: Automatically move Holmake object files to sigobj

This simplifies handling of files that we want to use in core HOL
modules. Under Poly/ML, the same object files are already loaded into
the buildheap tool so the hacking of sigobj doesn't need to happen.

Along the way, make sure the regression test for issue #451 also works
properly under Moscow ML.

Fix a number of Holmakefiles to use CLINE_OPTIONS

All uses of OPTIONS should eventually be removed

Move FunctionalRecordUpdate.sml to tools/Holmake

This is from tools-poly/Holmake. Reason is that I want as little code
as possible in tools-poly; everything that stands the least chance of
being shared should be in tools, not tools-poly.

Move GetOpt.{sig,sml} to Holmake directory

I think I should be using this code to process Holmake's many
command-line options.

Ensure FunctionalRecordUpdate .uo file is made

This required a change to src/portableML's Holmakefile so that the .uo
file was a target.

I hadn't properly tested 6f30f72194

Update to new FunctionalRecordUpdate tech

This is from the mlton.org (as per URL in checked-in file). Also move
the source file to the Holmake directory so that I can use it there. The
Holmakefile in src/portableML then copies it from that location into
position so that it properly ends up in sigobj etc.

This version of the file supposedly compiles faster, and it also seems
to handle polymorphic fields.

Empty command-line Holmake only builds first target in Holmakefile.

If there is no Holmakefile, or if there is a Holmakefile with no
targets, then the old behaviour of attempting to build everything
possible happens.

Documented in release notes and DESCRIPTION.

Many of the distribution's Holmakefiles were harmed in the creation of
this commit, but, for the reasons given in the release notes, I don't
think this should happen that often for typical user developments.

Closes #175

Fix bug in Redblackset.isSubset (empty sets were only subsets of empty sets)

This came up while investigating github issue #113

The Moscow ML Holmake was not recording the dependency on basis2002.uo
correctly. Now that it does, the attempt to do it explicitly in
src/portableML/Holmakefile can be dropped.

Implement more of Basis2002 for Moscow ML (adding Vector, Array,
ArraySlice and VectorSlice), simplifying what Poly/ML has to emulate.
Haven't done full rebuild test, but have got as far as integerTheory
and Omega, which makes heavy uses of Vector etc.

No idea about what is new with this.

New Kananaskis Makefile needs to tell the system not to use the overlay
file.