PURE_SIMP_CONV : thm list -> conv
Simplify a term repeatedly by conditional contextual rewriting, not using
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.
- SEE ALSO
PURE_REWRITE_CONV, SIMP_CONV, SIMP_RULE, SIMP_TAC.