PURE_SIMP_RULE : thm list -> thm -> thm
Simplify conclusion of a theorem repeatedly by conditional contextual
rewriting, not using default simplifications.
A call SIMP_CONV thl (|- tm) will return |- tm' where tm' results from
applying the theorems in thl as (conditional) rewrite rules. Howver, the
PURE prefix indicates that it will not automatically include the usual
built-in simplifications (see basic_rewrites and basic_convs). For more
details on this kind of conditional rewriting, see SIMP_CONV.
- FAILURE CONDITIONS
Never fails, but may return the input theorem unchanged if no simplifications
- SEE ALSO
ONCE_SIMP_RULE, SIMP_CONV, SIMP_RULE, SIMP_TAC.