FILTER_PURE_ONCE_ASM_REWRITE_RULE : ((term -> bool) -> thm list -> thm -> thm)
STRUCTURE
SYNOPSIS
Rewrites a theorem once using some of its assumptions.
DESCRIPTION
The first argument is a predicate applied to the assumptions. The theorem is rewritten with the assumptions for which the predicate returns true and the given list of theorems. It searches the term of the theorem once, without applying rewrites recursively. Thus it avoids the divergence which can result from the application of FILTER_PURE_ASM_REWRITE_RULE. For more information on rewriting rules, see GEN_REWRITE_RULE.
FAILURE
Never fails.
USES
This function is useful when rewriting with a subset of assumptions of a theorem, allowing control of the number of rewriting passes.
SEEALSO
HOL  Kananaskis-13