ONCE_ASM_REWRITE_TAC : (thm list -> tactic)
STRUCTURE
Rewrite
SYNOPSIS
Rewrites a goal once including built-in rewrites and the goal’s assumptions.
DESCRIPTION
ONCE_ASM_REWRITE_TAC behaves in the same way as ASM_REWRITE_TAC, but makes one pass only through the term of the goal. The order in which the given theorems are applied is an implementation matter and the user should not depend on any ordering. See GEN_REWRITE_TAC for more information on rewriting a goal in HOL.
FAILURE
ONCE_ASM_REWRITE_TAC does not fail and, unlike ASM_REWRITE_TAC, does not diverge. The resulting tactic may not be valid, if the rewrites performed add new assumptions to the theorem eventually proved.
EXAMPLE
The use of ONCE_ASM_REWRITE_TAC to control the amount of rewriting performed is illustrated below: 
   - ONCE_ASM_REWRITE_TAC []
       ([Term` (a:'a) = b`, Term `(b:'a) = c`], Term `P (a:'a): bool`);

   > val it = ([([`a = b`, `b = c`], `P b`)], fn)
      : (term list * term) list * (thm list -> thm)


   - (ONCE_ASM_REWRITE_TAC [] THEN ONCE_ASM_REWRITE_TAC [])
     ([Term`(a:'a) = b`, Term`(b:'a) = c`], Term `P (a:'a): bool`);

   > val it = ([([`a = b`, `b = c`], `P c`)], fn)
      : (term list * term) list * (thm list -> thm)

USES
ONCE_ASM_REWRITE_TAC can be applied once or iterated as required to give the effect of ASM_REWRITE_TAC, either to avoid divergence or to save inference steps.
SEEALSO
ASM_REWRITE_TAC, FILTER_ASM_REWRITE_TAC, FILTER_ONCE_ASM_REWRITE_TAC, GEN_REWRITE_TAC, ONCE_ASM_REWRITE_TAC, ONCE_REWRITE_TAC, PURE_ASM_REWRITE_TAC, PURE_ONCE_ASM_REWRITE_TAC, PURE_ONCE_REWRITE_TAC, PURE_REWRITE_TAC, REWRITE_TAC, SUBST_TAC
HOL  Kananaskis-13