PURE_ONCE_ASM_REWRITE_TAC : (thm list -> tactic)

- STRUCTURE
- SYNOPSIS
- 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.
- SEEALSO

HOL Kananaskis-14