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.