Again allow ancestral data to consume deltas all at once on theory-load

This allows named simpset-fragments to be added to srw_ss. This then
allows those fragments to be easily removed with calls to
diminish_srw_ss. In the 'fix-ancestry' rework this ability was
removed but this did break proofs when diminish_srw_ss calls had no
effect.

Selftest in coretypes demonstrates this with removal of the "one"
fragment.

Fixes to make sure that uptodate checks work properly

Existing regression tests now pass

Present IndDefLib's rule-induction-map as a theorem-set with ancestry

Only required change to the underlying API is to acknowledge that a
call to merge may result in no value if none of the desired parents
have a value either.

Add export_with_ancestry to ThmSetData signature

It compiles but is completely untested

Tweak ThmSetData API: take callbacks with more honest types

In particular, the callbacks are always only ever called on singleton
lists, so it seems silly to ask the user for functions with types that
have lists.

Change "thm-names" (used in various places) to be Thy-Name record

This saves on pulling things apart and looking for dots and the like.
It changes the simpLib API (most significantly for the SSFRAG function
which builds simpset fragments).

Rework ThmSetData implementation to use Theory s-expressions

This makes the encoding more robust, particularly if set "removal
instructions" might include space characters.

Refactor handling of thm attributes ("simp", etc) into new module

A slight backwards incompatibility is that this removes the ability
for script files to declare new attributes (hence removal of
attr[12]Script.sml from src/1/theory_tests). This facility is used
vacuously in CakeML once.

Rework persistent ThmSetData API to allow for "removal" of elements

The removals are strings encoding removal "instructions", which are up
to the underlying consumer to interpret. Still to test any of this
new machinery, but the old behaviours have been preserved.

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).

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.

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.

Provide lookup functionality across all stored theorem sets.

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