PURE_ONCE_ASM_REWRITE_RULE

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

Rewrites a theorem once, including the theorem’s assumptions as rewrites.

PURE_ONCE_ASM_REWRITE_RULE excludes the basic tautologies in implicit_rewrites from the theorems used for rewriting. It searches for matching subterms once only, without recursing over already rewritten subterms. For a general introduction to rewriting tools see GEN_REWRITE_RULE.

Failure

PURE_ONCE_ASM_REWRITE_RULE does not fail and does not diverge.

See also

Rewrite.ASM_REWRITE_RULE, Rewrite.GEN_REWRITE_RULE, Rewrite.ONCE_ASM_REWRITE_RULE, Rewrite.ONCE_REWRITE_RULE, Rewrite.PURE_ASM_REWRITE_RULE, Rewrite.PURE_REWRITE_RULE, Rewrite.REWRITE_RULE