PURE_REWRITE_RULE : thm list -> thm -> thm
- SYNOPSIS
-
Rewrites a theorem with only the given list of rewrites.
- DESCRIPTION
-
This rule provides a method for rewriting a theorem with the theorems given,
and excluding simplification with tautologies in basic_rewrites. Matching
subterms are found recursively starting from the term in the conclusion part of
the theorem, until no more matches are found. For more details on rewriting see
GEN_REWRITE_RULE.
- USES
-
PURE_REWRITE_RULE 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_RULE can be used.
- SEE ALSO
-
ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_REWRITE_RULE,
PURE_ASM_REWRITE_RULE, PURE_ONCE_ASM_REWRITE_RULE,
PURE_ONCE_REWRITE_RULE, REWRITE_RULE.