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.

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