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
|
\DOC PURE_ONCE_REWRITE_RULE
\TYPE {PURE_ONCE_REWRITE_RULE : thm list -> thm -> thm}
\SYNOPSIS
Rewrites a theorem once with only the given list of rewrites.
\KEYWORDS
rule.
\DESCRIBE
{PURE_ONCE_REWRITE_RULE} generates rewrites from the list of theorems
supplied by the user, without including the tautologies given in
{basic_rewrites}. The applicable rewrites are employed once, without
entailing in a recursive search for matches over the theorem.
See {GEN_REWRITE_RULE} for more details about rewriting strategies in
HOL.
\FAILURE
This rule does not fail, and it does not diverge.
\SEEALSO
ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_DEPTH_CONV,
ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE.
\ENDDOC
|
