ONCE_ASM_REWRITE_RULE

Rewrite.ONCE_ASM_REWRITE_RULE : (thm list -> thm -> thm)

Rewrites a theorem once including built-in rewrites and the theorem’s assumptions.

ONCE_ASM_REWRITE_RULE applies all possible rewrites in one step over the subterms in the conclusion of the theorem, but stops after rewriting at most once at each subterm. This strategy is specified as for ONCE_DEPTH_CONV. For more details see ASM_REWRITE_RULE, which does search recursively (to any depth) for matching subterms. The general strategy for rewriting theorems is described under GEN_REWRITE_RULE.

Failure

Never fails.

This tactic is used when rewriting with the hypotheses of a theorem (as well as a given list of theorems and implicit_rewrites), when more than one pass is not required or would result in divergence.

See also

Rewrite.ASM_REWRITE_RULE, Rewrite.FILTER_ASM_REWRITE_RULE, Rewrite.FILTER_ONCE_ASM_REWRITE_RULE, Rewrite.GEN_REWRITE_RULE, Conv.ONCE_DEPTH_CONV, Rewrite.ONCE_REWRITE_RULE, Rewrite.PURE_ASM_REWRITE_RULE, Rewrite.PURE_ONCE_ASM_REWRITE_RULE, Rewrite.PURE_REWRITE_RULE, Rewrite.REWRITE_RULE