----------------------------------------------------------------------
PURE_ONCE_REWRITE_TAC                                        (Rewrite)
----------------------------------------------------------------------
PURE_ONCE_REWRITE_TAC : (thm list -> tactic)

SYNOPSIS
Rewrites a goal using a supplied list of theorems, making one
rewriting pass over the goal.

KEYWORDS
tactic.

DESCRIBE
{PURE_ONCE_REWRITE_TAC} generates a set of rewrites from the given
list of theorems, and applies them at every match found through
searching once over the term part of the goal, without recursing. It
does not include the basic tautologies as rewrite theorems. The order
in which the rewrites are applied is unspecified. For more information
on rewriting tactics see {GEN_REWRITE_TAC}.

FAILURE
{PURE_ONCE_REWRITE_TAC} does not fail and does not diverge.

USES
This tactic is useful when the built-in tautologies are not required
as rewrite equations and recursive rewriting is not desired.

SEEALSO
Rewrite.ASM_REWRITE_TAC, Rewrite.GEN_REWRITE_TAC,
Rewrite.FILTER_ASM_REWRITE_TAC, Rewrite.FILTER_ONCE_ASM_REWRITE_TAC,
Rewrite.ONCE_ASM_REWRITE_TAC, Rewrite.ONCE_REWRITE_TAC,
Rewrite.PURE_ASM_REWRITE_TAC, Rewrite.PURE_ONCE_ASM_REWRITE_TAC,
Rewrite.PURE_REWRITE_TAC, Rewrite.REWRITE_TAC, Tactic.SUBST_TAC.

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