Rewrites a goal once, including the goal’s assumptions as rewrites.
DESCRIPTION
A set of rewrites generated from the assumptions of the goal and the
supplied theorems is used to rewrite the term part of the goal, making
only one pass over the goal. The basic tautologies are not included as
rewrite theorems. 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
tactics in general.
FAILURE
PURE_ONCE_ASM_REWRITE_TAC does not fail and does not diverge.
USES
Manipulation of the goal by rewriting with its assumptions, in
instances where rewriting with tautologies and recursive rewriting is
undesirable.