Rewrite.add_implicit_rewrites: thm list -> unit
STRUCTURE
SYNOPSIS
Augments the built-in database of simplifications automatically included in rewriting.
USES
Used to build up the power of the built-in simplification set.
SEEALSO
HOL  Kananaskis-13