Update help for BasicProvers.export_rewrites and thy_ssfrag

Document export_rewrites' ability to export rewrites from other segments.

Changed a couple of misleading/annoying names. The type ssdata is now
called ssfrag (to bring it into line with documentation that talks about
simpset fragments), and the constructor SIMPSET is now called SSFRAG.
It never created a simpset, so the latter was a stupid name.

Typo correction.

Modify export_rewrites to allow for multiple calls to this function
within a session. This makes it easier to ensure theorems are exported;
they can have this done at point of proof, rather than needing to be
gathered together at the end of the file. The idiom for getting this
done is based on the way grm_updates is handled in Parse.sml (an idea of
Konrad's); note the funky use of a reference variable within a closure's
environment.

Last minute doc changes.

Documentation of the ``stateful rewriting system''.