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

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

KEYWORDS
tactic.

DESCRIBE
{DEP_PURE_REWRITE_TAC} is to {DEP_REWRITE_TAC} what {PURE_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.

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.

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