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_CONV
\TYPE {PURE_ONCE_REWRITE_CONV : thm list -> conv}
\SYNOPSIS
Rewrites a term once with only the given list of rewrites.
\KEYWORDS
conversion.
\DESCRIBE
{PURE_ONCE_REWRITE_CONV} 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 term.
See {GEN_REWRITE_CONV} for more details about rewriting strategies in
HOL.
\FAILURE
This rule does not fail, and it does not diverge.
\SEEALSO
GEN_REWRITE_CONV, ONCE_DEPTH_CONV,
ONCE_REWRITE_CONV, PURE_REWRITE_CONV, REWRITE_CONV.
\ENDDOC
|
