Simplify a goal repeatedly by conditional contextual rewriting without default
simplifications.
DESCRIPTION
When applied to a goal A ?- g, the tactic PURE_SIMP_TAC thl returns a new
goal A ?- g' where g' results from applying the theorems in thl as
(conditional) rewrite rules. The PURE prefix means that it does not apply the
built-in simplifications (see basic_rewrites and basic_convs). For more
details, see SIMP_CONV.
FAILURE CONDITIONS
Never fails, though may not change the goal if no simplifications are
applicable.
COMMENTS
To add the assumptions of the goal to the rewrites, use PURE_ASM_SIMP_TAC (or
just ASM PURE_SIMP_TAC).