PURE_ONCE_REWRITE_RULE : thm list -> thm -> thm

- SYNOPSIS
- Rewrites a theorem once with only the given list of rewrites.
- DESCRIPTION
- PURE_ONCE_REWRITE_RULE generates rewrites from the list of theorems supplied by the user, without including the tautologies given in basic_rewrites. The applicable rewrites are employed once, without entailing in a recursive search for matches over the theorem. See GEN_REWRITE_RULE for more details about rewriting strategies in HOL.
- FAILURE CONDITIONS
- This rule does not fail, and it does not diverge.
- SEE ALSO
- ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_DEPTH_CONV, ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE.