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
|
\DOC PURE_REWRITE_CONV
\TYPE {PURE_REWRITE_CONV : thm list -> conv}
\SYNOPSIS
Rewrites a term with only the given list of rewrites.
\KEYWORDS
conversion.
\DESCRIBE
This conversion provides a method for rewriting a term with the theorems given,
and excluding simplification with tautologies in {basic_rewrites}. Matching
subterms are found recursively, until no more matches are found.
For more details on rewriting see
{GEN_REWRITE_CONV}.
\USES
{PURE_REWRITE_CONV} is useful when the simplifications that arise by
rewriting a theorem with {basic_rewrites} are not wanted.
\FAILURE
Does not fail. May result in divergence, in which case
{PURE_ONCE_REWRITE_CONV} can be used.
\SEEALSO
GEN_REWRITE_CONV, ONCE_REWRITE_CONV, PURE_ONCE_REWRITE_CONV, REWRITE_CONV.
\ENDDOC
|
