PURE_ASM_SIMP_TAC : thm list -> tactic
Perform simplification of goal by conditional contextual rewriting using
A call to PURE_ASM_SIMP_TAC[theorems] will apply conditional contextual
rewriting with theorems and the current assumptions of the goal to the goal's
conclusion, but not the default simplifications (see basic_rewrites and
basic_convs). For more details on this kind of rewriting, see SIMP_CONV. If
the extra generality of contextual conditional rewriting is not needed,
REWRITE_TAC is usually more efficient.
- FAILURE CONDITIONS
Never fails, but may loop indefinitely.
- SEE ALSO
ASM_REWRITE_TAC, ASM_SIMP_TAC, SIMP_CONV, SIMP_TAC, REWRITE_TAC.