PURE_ONCE_REWRITE_TAC

Rewrite.PURE_ONCE_REWRITE_TAC : (thm list -> tactic)

Rewrites a goal using a supplied list of theorems, making one rewriting pass over the goal.

PURE_ONCE_REWRITE_TAC generates a set of rewrites from the given list of theorems, and applies them at every match found through searching once over the term part of the goal, without recursing. It does not include the basic tautologies as rewrite theorems. The order in which the rewrites are applied is unspecified. For more information on rewriting tactics see GEN_REWRITE_TAC.

Failure

PURE_ONCE_REWRITE_TAC does not fail and does not diverge.

This tactic is useful when the built-in tautologies are not required as rewrite equations and recursive rewriting is not desired.

See also

Rewrite.ASM_REWRITE_TAC, Rewrite.GEN_REWRITE_TAC, Rewrite.FILTER_ASM_REWRITE_TAC, Rewrite.FILTER_ONCE_ASM_REWRITE_TAC, Rewrite.ONCE_ASM_REWRITE_TAC, Rewrite.ONCE_REWRITE_TAC, Rewrite.PURE_ASM_REWRITE_TAC, Rewrite.PURE_ONCE_ASM_REWRITE_TAC, Rewrite.PURE_REWRITE_TAC, Rewrite.REWRITE_TAC, Tactic.SUBST_TAC