1\DOC add_implicit_rewrites 2 3\TYPE {Rewrite.add_implicit_rewrites: thm list -> unit} 4 5\SYNOPSIS 6Augments the built-in database of simplifications automatically included in 7rewriting. 8 9\USES 10Used to build up the power of the built-in simplification set. 11 12\SEEALSO 13Rewrite.set_implicit_rewrites. 14 15\ENDDOC 16