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
31
32
33
34
35
|
\DOC ONCE_ASM_REWRITE_RULE
\TYPE {ONCE_ASM_REWRITE_RULE : (thm list -> thm -> thm)}
\SYNOPSIS
Rewrites a theorem once including built-in rewrites and the theorem's
assumptions.
\KEYWORDS
rule.
\DESCRIBE
{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.
\USES
This tactic is used when rewriting with the hypotheses of a theorem
(as well as a given list of theorems and {basic_rewrites}), when more
than one pass is not required or would result in divergence.
\SEEALSO
ASM_REWRITE_RULE, FILTER_ASM_REWRITE_RULE,
FILTER_ONCE_ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_DEPTH_CONV,
ONCE_REWRITE_RULE, PURE_ASM_REWRITE_RULE, PURE_ONCE_ASM_REWRITE_RULE,
PURE_REWRITE_RULE, REWRITE_RULE.
\ENDDOC
|
