----------------------------------------------------------------------
PURE_ASM_REWRITE_TAC                                         (Rewrite)
----------------------------------------------------------------------
PURE_ASM_REWRITE_TAC : (thm list -> tactic)

SYNOPSIS
Rewrites a goal including the goal’s assumptions as rewrites.

KEYWORDS
tactic.

DESCRIBE
{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
tactics.

FAILURE
{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.

USES
To advance or solve a goal when the current assumptions are expected
to be useful in reducing the goal.

SEEALSO
Rewrite.ASM_REWRITE_TAC, Rewrite.GEN_REWRITE_TAC,
Rewrite.FILTER_ASM_REWRITE_TAC, Rewrite.FILTER_ONCE_ASM_REWRITE_TAC,
Rewrite.ONCE_ASM_REWRITE_TAC, Rewrite.ONCE_REWRITE_TAC,
Rewrite.PURE_ONCE_ASM_REWRITE_TAC, Rewrite.PURE_ONCE_REWRITE_TAC,
Rewrite.PURE_REWRITE_TAC, Rewrite.REWRITE_TAC, Tactic.SUBST_TAC.

----------------------------------------------------------------------