[strub]

hint simplify disable L1, L2.
hint simplify enable L1, L2.
hint simplify in db : disable L.

switch the user-reduction rules compiled from the lemmas L1, L2
(in the default database, or in db) off, and back on, for the rest
of the enclosing theory / section of the current file. Every
simplification path is affected: simplify, /=, //, done,
trivial, auto, rewriting and conversion. An explicit per-call
(simplify hint {L}) or proof-local (hint {L}) addition still
fires, as it does not go through the database. Disabling a lemma that
has no rule in the database, or enabling one that is not disabled, is
an error.

The switches are independent from hint simplify L, which feeds the
database: adding a disabled lemma again does not switch it back on,
only enable does. And they are deliberately not theory items: they
are never exported to the files requiring this one -- a file able to
switch off rules in its clients would be a nightmare -- and they end
with the enclosing theory or section, whose environment is dropped
when it is closed. The implementation is a per-database mask of lemma
paths in the environment, applied when the rules of a head symbol are
fetched.

The motivating case is Jasmin's eclib hint simplify powS_minus@1,
which makes every simplification unroll 2^1024 again and again in
the files that use it; those files can now switch it off for
themselves.

print hint simplify reflects the switches and drops the heads left
without rules.