1\DOC PURE_REWRITE_CONV
2
3\TYPE {PURE_REWRITE_CONV : (thm list -> conv)}
4
5\SYNOPSIS
6Rewrites a term with only the given list of rewrites.
7
8\KEYWORDS
9conversion.
10
11\DESCRIBE
12This conversion provides a method for rewriting a term with the theorems given,
13and excluding simplification with tautologies in {implicit_rewrites}. Matching
14subterms are found recursively, until no more matches are found.
15For more details on rewriting see
16{GEN_REWRITE_CONV}.
17
18\USES
19{PURE_REWRITE_CONV} is useful when the simplifications that arise by
20rewriting a theorem with {implicit_rewrites} are not wanted.
21
22\FAILURE
23Does not fail. May result in divergence, in which case
24{PURE_ONCE_REWRITE_CONV} can be used.
25
26\SEEALSO
27Rewrite.GEN_REWRITE_CONV, Rewrite.ONCE_REWRITE_CONV, Rewrite.PURE_ONCE_REWRITE_CONV, Rewrite.REWRITE_CONV.
28\ENDDOC
29