DEP_ASM_REWRITE_TAC

dep_rewrite.DEP_ASM_REWRITE_TAC : thm list -> tactic

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

DEP_ASM_REWRITE_TAC is to DEP_REWRITE_TAC what ASM_REWRITE_TAC is to REWRITE_TAC.

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

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