DEP_ONCE_REWRITE_TAC

dep_rewrite.DEP_ONCE_REWRITE_TAC : thm list -> tactic

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

DEP_ONCE_REWRITE_TAC is to DEP_REWRITE_TAC what ONCE_REWRITE_TAC is to REWRITE_TAC.

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.

See also

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