----------------------------------------------------------------------
ONCE_REWRITE_CONV                                            (Rewrite)
----------------------------------------------------------------------
ONCE_REWRITE_CONV : (thm list -> conv)

SYNOPSIS
Rewrites a term, including built-in tautologies in the list of rewrites.

KEYWORDS
conversion.

DESCRIBE
{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
{implicit_rewrites}. See {GEN_REWRITE_CONV} for the general method of
using theorems to rewrite a term.

FAILURE
{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.

SEEALSO
Rewrite.GEN_REWRITE_CONV, Rewrite.PURE_ONCE_REWRITE_CONV,
Rewrite.PURE_REWRITE_CONV, Rewrite.REWRITE_CONV.

----------------------------------------------------------------------