DEP_PURE_ASM_REWRITE_TAC

dep_rewrite.DEP_PURE_ASM_REWRITE_TAC : thm list -> tactic

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

DEP_PURE_ASM_REWRITE_TAC is to DEP_REWRITE_TAC what PURE_ASM_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 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