add_implicit_rewrites

Rewrite.add_implicit_rewrites: thm list -> unit

Augments the built-in database of simplifications automatically included in rewriting.

Used to build up the power of the built-in simplification set.

See also

Rewrite.set_implicit_rewrites