Move smpp to Portable - get everything up to arithmeticScript working

Up to and boolTheory and slightly beyond

Give Theory Data writers access to term-writing

Just as readers get an additional parameter of type string -> term,
writers will get a parameter of type term -> string.

Make theory data types provide terms function

This function takes a value of the theory-data type and returns a list
of terms that are contained inside this value. The machinery will use
that to prime the theory's sharing tables to allow for efficient
recording of terms in data.

Give ThyData access to a term-reader function

No useful way to exploit this just yet, but the code compiles and I
think the refactoring is right.

ThmSetData passes thms *and* names to consumers

The names were always available, but the API now changes so that
consumers get names as well as theorem values. They can ignore the
names of course. (In this context, consumers are things like the
stateful rewriter, the monotonicity rule database, the TFL congruence
rule database etc.)

This will be helpful in allowing the stateful simpset to know what its
theorems are called, which is progress with Github issue #313 (to allow
easy removal of rewrites from a call to the simplifier).

Bug fix (w/test case) for ThmSetData's new way to add theorems

Problem was that the callback function attached to the set didn't get
called, even though the theorem was successfully exported. This meant
that a set like "simp" (which feeds into srw_ss()) didn't prompt any
change to the stateful simpset. Being successfully exported did at
least mean that the theorem would get into the simpset in descendent
theories.

Test for ThmSetData bug fixed in 8ffc5dc0b; prettify adjoined SML output

Fix bug in SML emitted/adjoined by new_storage_attribute.

Implement new scheme to allow simple addition of theorems to theorem "sets".

When saving or storing theorems, simply add [name1,name2] strings to the
end of the binding, and the theorem being saved will be added to the
theorem set with that name.

Make ThmSetData handle empty/null data as input.

Closes #130

Get better diagnostic messages out of ThmSetData warnings.

Use hook for binding-deletion to make ThmSetData more robust.

Test-case also uses WARNINGs_as_ERRs to check that nothing untoward
gets warned about in the second theory (the one that imports the
theory which has had lots of delete_{const,binding} events).

Adjust (and reduce) interface to ThmSetData.

The change is to add an extra string parameter to the callback
function that the client provides. This is the name of the theory
which has stored the theorems. This change prompted the changes to
computeLib, IndDefLib and DefnBase.

The reduction was to remove the ThmSetData's new function, forcing
BasicProvers to use new_exporter. This was possible because of the
extra information provided to its call-back.

I also wrote some test-cases mimicking the original problem that
Magnus and Ramana had, and prettied the warning output.

This closes #73.

Get stored ThmSets to notice deletion of relevant consts.

This is progress with #73.

Provide lookup functionality across all stored theorem sets.

Rework various Theory hooks into one general framework.

The basis for the framework is the TheoryDelta type. Client code can
ask to be notified of theory changes, and will have their provided
call-back function called at appropriate times.

This commit hasn't adjusted the theory functions for
{add,del}{const/typeOp} yet; it has just unified the existing
functionality (register_onload, after_new_theory and
register_onexport).

Make theorem-set loading more robust in face of bad thm-names.

Most attempts to mess with the data will be caught at specification
time, but use of delete_const and friends can cause theorems to not
get exported even if they were present when the call to export_X was
made.

Delete some unused code in ThmSetData.sml

Change src/bool to src/1 as a prelude to experimentation!