Simplify a term repeatedly by conditional contextual rewriting, not using
default simplifications.
DESCRIPTION
A call SIMP_CONV thl tm will return |- tm = tm' where tm' results from
applying the theorems in thl as (conditional) rewrite rules. This is similar
to SIMP_CONV, and the documentation for that contains more details. The
PURE prefix means that the usual built-in simplifications (see
basic_rewrites and basic_convs) are not applied.
FAILURE CONDITIONS
Never fails, but may return a reflexive theorem |- tm = tm if no
simplifications can be made.