ONCE_REWRITE_RULE : thm list -> thm -> thm
Rewrites a theorem, including built-in tautologies in the list of rewrites.
ONCE_REWRITE_RULE searches for matching subterms and applies
rewrites once at each subterm, in the manner specified for
ONCE_DEPTH_CONV. The rewrites which are used are obtained from the
given list of theorems and the set of tautologies stored in
basic_rewrites. See GEN_REWRITE_RULE for the general method of
using theorems to rewrite an object theorem.
- FAILURE CONDITIONS
ONCE_REWRITE_RULE does not fail; it does not diverge.
ONCE_REWRITE_RULE can be used to rewrite a theorem when recursive
rewriting is not desired.
- SEE ALSO
ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_ASM_REWRITE_RULE,
PURE_ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE.