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