----------------------------------------------------------------------
PURE_ASM_REWRITE_RULE                                        (Rewrite)
----------------------------------------------------------------------
PURE_ASM_REWRITE_RULE : (thm list -> thm -> thm)

SYNOPSIS
Rewrites a theorem including the theorem’s assumptions as rewrites.

KEYWORDS
rule.

DESCRIBE
The list of theorems supplied by the user and the assumptions of the
object theorem are used to generate a set of rewrites, without adding
implicitly the basic tautologies stored under {implicit_rewrites}.
The rule searches for matching subterms in a top-down recursive
fashion, stopping only when no more rewrites apply. For a general
description of rewriting strategies see {GEN_REWRITE_RULE}.

FAILURE
Rewriting with {PURE_ASM_REWRITE_RULE} does not result in failure. It
may diverge, in which case {PURE_ONCE_ASM_REWRITE_RULE} may be used.

SEEALSO
Rewrite.ASM_REWRITE_RULE, Rewrite.GEN_REWRITE_RULE,
Rewrite.ONCE_REWRITE_RULE, Rewrite.PURE_REWRITE_RULE,
Rewrite.PURE_ONCE_ASM_REWRITE_RULE.

----------------------------------------------------------------------