DEP_PURE_ONCE_REWRITE_TAC is to DEP_REWRITE_TAC what PURE_ONCE_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 including ONCE in their name attempt to use each theorem in the list, only once, in order, left to right. The hypotheses added in the process of dependent rewriting are not rewritten by the ONCE tactics. This gives a more restrained version of dependent rewriting.

The tactics without ONCE or LIST attempt to reuse all theorems repeatedly, continuing to rewrite until no changes can be achieved in the goal. Hypotheses are rewritten as well, and their hypotheses as well, ad infinitum.

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