REWRITE_TAC : (thm list -> tactic)
REWRITE_TAC transforms (or solves) a goal by using as rewrite rules (i.e. as left-to-right replacement rules) the conclusions of the given list of (equational) theorems, as well as a set of built-in theorems (common tautologies) held in the ML variable implicit_rewrites. Recognition of a tautology often terminates the subgoaling process (i.e. solves the goal).
The equational rewrites generated are applied recursively and to arbitrary depth, with matching and instantiation of variables and type variables. A list of rewrites can set off an infinite rewriting process, and it is not, of course, decidable in general whether a rewrite set has that property. The order in which the rewrite theorems are applied is unspecified, and the user should not depend on any ordering.
See GEN_REWRITE_TAC for more details on the rewriting process. Variants of REWRITE_TAC allow the use of a different set of rewrites. Some of them, such as PURE_REWRITE_TAC, exclude the basic tautologies from the possible transformations. ASM_REWRITE_TAC and others include the assumptions at the goal in the set of possible rewrites.
Still other tactics allow greater control over the search for rewritable subterms. Several of them such as ONCE_REWRITE_TAC do not apply rewrites recursively. GEN_REWRITE_TAC allows a rewrite to be applied at a particular subterm.
- REWRITE_TAC [GREATER_DEF] (,``5 > 4``); > ([(, ``4 < 5``)], -) : subgoals
- val (gl,p) = REWRITE_TAC [GREATER_DEF, LESS_0] (,``(SUC n) > 0``); > val gl =  : goal list > val p = fn : proof - p; > val it = |- (SUC n) > 0 : thm
REWRITE_TAC may be more powerful a tactic than is needed in certain situations; if efficiency is at stake, alternatives might be considered. On the other hand, if more power is required, the simplification functions (SIMP_TAC and others) may be appropriate.