PURE_ONCE_REWRITE_CONV : thm list -> conv
- SYNOPSIS
-
Rewrites a term once with only the given list of rewrites.
- DESCRIPTION
-
PURE_ONCE_REWRITE_CONV 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 term.
See GEN_REWRITE_CONV for more details about rewriting strategies in
HOL.
- FAILURE CONDITIONS
-
This rule does not fail, and it does not diverge.
- SEE ALSO
-
GEN_REWRITE_CONV, ONCE_DEPTH_CONV,
ONCE_REWRITE_CONV, PURE_REWRITE_CONV, REWRITE_CONV.