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