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