Rewrites a theorem once including built-in rewrites and the theorem’s
assumptions.
DESCRIPTION
ONCE_ASM_REWRITE_RULE applies all possible rewrites in one step
over the subterms in the conclusion of the theorem, but stops after
rewriting at most once at each subterm. This strategy is specified as
for ONCE_DEPTH_CONV. For more details see ASM_REWRITE_RULE, which
does search recursively (to any depth) for matching subterms. The
general strategy for rewriting theorems is described under
GEN_REWRITE_RULE.
FAILURE
Never fails.
USES
This tactic is used when rewriting with the hypotheses of a theorem
(as well as a given list of theorems and implicit_rewrites), when more
than one pass is not required or would result in divergence.