PURE_ONCE_ASM_REWRITE_RULE : thm list -> thm -> thm

- SYNOPSIS
- Rewrites a theorem once, including the theorem's assumptions as rewrites.
- DESCRIPTION
- PURE_ONCE_ASM_REWRITE_RULE excludes the basic tautologies in basic_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 CONDITIONS
- PURE_ONCE_ASM_REWRITE_RULE does not fail and does not diverge.
- SEE ALSO
- ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_ASM_REWRITE_RULE, ONCE_REWRITE_RULE, PURE_ASM_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE.