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.

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

Test demonstrating the problem with github issue #130