PURE_REWRITE_CONV : thm list -> conv
- SYNOPSIS
-
Rewrites a term with only the given list of rewrites.
- DESCRIPTION
-
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 CONDITIONS
-
Does not fail. May result in divergence, in which case
PURE_ONCE_REWRITE_CONV can be used.
- SEE ALSO
-
GEN_REWRITE_CONV, ONCE_REWRITE_CONV, PURE_ONCE_REWRITE_CONV, REWRITE_CONV.