PURE_ASM_REWRITE_TAC : thm list -> tactic
Rewrites a goal including the goal's assumptions as rewrites.
PURE_ASM_REWRITE_TAC generates a set of rewrites from the supplied
theorems and the assumptions of the goal, and applies these in a
top-down recursive manner until no match is found. See
GEN_REWRITE_TAC for more information on the group of rewriting
- FAILURE CONDITIONS
PURE_ASM_REWRITE_TAC does not fail, but it can diverge in certain
situations. For limited depth rewriting, see
PURE_ONCE_ASM_REWRITE_TAC. It can also result in an invalid tactic.
To advance or solve a goal when the current assumptions are expected
to be useful in reducing the goal.
- SEE ALSO
ASM_REWRITE_TAC, GEN_REWRITE_TAC, ONCE_ASM_REWRITE_TAC, ONCE_REWRITE_TAC,
PURE_ONCE_ASM_REWRITE_TAC, PURE_ONCE_REWRITE_TAC, PURE_REWRITE_TAC,
REWRITE_TAC, SUBST_ALL_TAC, SUBST1_TAC.