PURE_ONCE_ASM_REWRITE_RULE : (thm list -> thm -> thm)
STRUCTURE
SYNOPSIS
Rewrites a theorem once, including the theorem’s assumptions as rewrites.
DESCRIPTION
PURE_ONCE_ASM_REWRITE_RULE excludes the basic tautologies in implicit_rewrites from the theorems used for rewriting. It searches for matching subterms once only, without recursing over already rewritten subterms. For a general introduction to rewriting tools see GEN_REWRITE_RULE.
FAILURE
PURE_ONCE_ASM_REWRITE_RULE does not fail and does not diverge.
SEEALSO
HOL  Trindemossen-1