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-14