ASM_SIMP_TAC : thm list -> tactic

SYNOPSIS
Perform simplification of goal by conditional contextual rewriting using assumptions and built-in simplifications.

DESCRIPTION
A call to ASM_SIMP_TAC[theorems] will apply conditional contextual rewriting with theorems and the current assumptions of the goal to the goal's conclusion, as well as 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, SIMP_CONV, SIMP_TAC, REWRITE_TAC.