----------------------------------------------------------------------
DEP_PURE_ASM_REWRITE_TAC                                 (dep_rewrite)
----------------------------------------------------------------------
DEP_PURE_ASM_REWRITE_TAC : thm list -> tactic

SYNOPSIS
Rewrites a goal using implications of equalites, adding proof obligations as required.

KEYWORDS
tactic.

DESCRIBE
{DEP_PURE_ASM_REWRITE_TAC} is to {DEP_REWRITE_TAC} what {PURE_ASM_REWRITE_TAC} is to {REWRITE_TAC}.

The tactics including PURE in their name will only use the
listed theorems for all rewriting; otherwise, the standard
rewrites are used for normal rewriting, but they are not
considered for dependent rewriting.

The tactics with ASM in their name add the assumption list to
the list of theorems used for dependent rewriting.

SEEALSO
dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC,
dep_rewrite.DEP_ONCE_REWRITE_TAC,
dep_rewrite.DEP_PURE_ONCE_ASM_REWRITE_TAC,
dep_rewrite.DEP_ONCE_ASM_REWRITE_TAC,
dep_rewrite.DEP_PURE_ONCE_SUBST_TAC, dep_rewrite.DEP_ONCE_SUBST_TAC,
dep_rewrite.DEP_PURE_ONCE_ASM_SUBST_TAC,
dep_rewrite.DEP_ONCE_ASM_SUBST_TAC,
dep_rewrite.DEP_PURE_LIST_REWRITE_TAC,
dep_rewrite.DEP_LIST_REWRITE_TAC,
dep_rewrite.DEP_PURE_LIST_ASM_REWRITE_TAC,
dep_rewrite.DEP_LIST_ASM_REWRITE_TAC,
dep_rewrite.DEP_PURE_REWRITE_TAC, dep_rewrite.DEP_REWRITE_TAC,
dep_rewrite.DEP_PURE_ASM_REWRITE_TAC, dep_rewrite.DEP_ASM_REWRITE_TAC,
dep_rewrite.DEP_FIND_THEN, dep_rewrite.DEP_LIST_FIND_THEN,
dep_rewrite.DEP_ONCE_FIND_THEN.

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