1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\DOC ONCE_REWRITE_RULE
\TYPE {ONCE_REWRITE_RULE : thm list -> thm -> thm}
\SYNOPSIS
Rewrites a theorem, including built-in tautologies in the list of rewrites.
\KEYWORDS
rule.
\DESCRIBE
{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
{ONCE_REWRITE_RULE} does not fail; it does not diverge.
\USES
{ONCE_REWRITE_RULE} can be used to rewrite a theorem when recursive
rewriting is not desired.
\SEEALSO
ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_ASM_REWRITE_RULE,
PURE_ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE.
\ENDDOC
|
