ONCE_ASM_SIMP_TAC : thm list -> tactic
Simplify toplevel applicable terms in goal using assumptions and context.
A call to ONCE_ASM_SIMP_TAC[theorems] will apply conditional contextual
rewriting with theorems and the current assumptions of the goal to the goal's
conclusion. The ONCE prefix means that the toplevel simplification is only
applied once to the toplevel terms, though any conditional subgoals generated
are then simplified repeatedly. For more details on this kind of rewriting, see
SIMP_CONV. If the extra generality of contextual conditional rewriting is not
needed, ONCE_ASM_REWRITE_TAC is usually more efficient.
- FAILURE CONDITIONS
Never fails, but may loop indefinitely.
- SEE ALSO
ASM_SIMP_TAC, ONCE_ASM_REWRITE_TAC, SIMP_CONV, SIMP_TAC, REWRITE_TAC.