ASM_REWRITE_RULE
Rewrite.ASM_REWRITE_RULE : thm list -> thm -> thm
Rewrites a theorem including built-in rewrites and the theorem's assumptions.
ASM_REWRITE_RULE rewrites using the tautologies in
implicit_rewrites, the given list of theorems, and the set of
hypotheses of the theorem. All hypotheses are used. No ordering is
specified among applicable rewrites. Matching subterms are searched for
recursively, starting with the entire term of the conclusion and
stopping when no rewritable expressions remain. For more details about
the rewriting process, see GEN_REWRITE_RULE. To avoid using the set of
basic tautologies, see PURE_ASM_REWRITE_RULE.
Failure
ASM_REWRITE_RULE does not fail, but may result in divergence. To
prevent divergence where it would occur, ONCE_ASM_REWRITE_RULE can be
used.
See also
Rewrite.GEN_REWRITE_RULE,
Rewrite.ONCE_ASM_REWRITE_RULE,
Rewrite.PURE_ASM_REWRITE_RULE,
Rewrite.PURE_ONCE_ASM_REWRITE_RULE,
Rewrite.REWRITE_RULE