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.