REWRITE_CONV : (thm list -> conv)
Variants of this conversion allow changes in the set of equations used: PURE_REWRITE_CONV and others in its family do not rewrite with the theorems in implicit_rewrites.
The top-down recursive search for matches may not be desirable, as this may increase the number of inferences being made or may result in divergence. In this case other rewriting tools such as ONCE_REWRITE_CONV and GEN_REWRITE_CONV can be used, or the set of theorems given may be reduced.
See GEN_REWRITE_CONV for the general strategy for simplifying theorems in HOL using equational theorems.