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

SYNOPSIS
Rewrites a term once with only the given list of rewrites.

KEYWORDS
conversion.

DESCRIBE
{PURE_ONCE_REWRITE_CONV} generates rewrites from the list of theorems
supplied by the user, without including the tautologies given in
{implicit_rewrites}. The applicable rewrites are employeded 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
This rule does not fail, and it does not diverge.

SEEALSO
Rewrite.GEN_REWRITE_CONV, Conv.ONCE_DEPTH_CONV,
Rewrite.ONCE_REWRITE_CONV, Rewrite.PURE_REWRITE_CONV,
Rewrite.REWRITE_CONV.

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