PURE_ONCE_REWRITE_TAC : (thm list -> tactic)
STRUCTURE
SYNOPSIS
Rewrites a goal using a supplied list of theorems, making one rewriting pass over the goal.
DESCRIPTION
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
HOL  Kananaskis-13