ASM_REWRITE_RULE : thm list -> thm -> thm
STRUCTURE
SYNOPSIS
Rewrites a theorem including built-in rewrites and the theorem’s assumptions.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1