ONCE_REWRITE_CONV : thm list -> conv
- SYNOPSIS
-
Rewrites a term, including built-in tautologies in the list of rewrites.
- DESCRIPTION
-
ONCE_REWRITE_CONV searches for matching subterms and applies
rewrites once at each subterm, in the manner specified for
ONCE_DEPTH_CONV. The rewrites which are used are obtained from the
given list of theorems and the set of tautologies stored in
basic_rewrites. See GEN_REWRITE_CONV for the general method of
using theorems to rewrite a term.
- FAILURE CONDITIONS
-
ONCE_REWRITE_CONV does not fail; it does not diverge.
- USES
-
ONCE_REWRITE_CONV can be used to rewrite a term when recursive
rewriting is not desired.
- SEE ALSO
-
GEN_REWRITE_CONV, PURE_ONCE_REWRITE_CONV, PURE_REWRITE_CONV, REWRITE_CONV.