----------------------------------------------------------------------
REWR_CONV_A                                                     (Conv)
----------------------------------------------------------------------
REWR_CONV_A : (thm -> conv)

SYNOPSIS
Uses an instance of a given equation to rewrite a term.

KEYWORDS
conversion.

DESCRIBE
{REWR_CONV_A th} behaves as
{REWR_CONV th} except that it allows substitution of variables or type
variables which appear in the hypotheses of {th}.

EXAMPLE
Consider the theorem {th}

   [0 < n] |- (a * n = b * (n : int)) <=> (a = b)

and the term {tm}

   f (a * m = b * (m : int)) x

Then {DEPTH_CONV (REWR_CONV_A th) tm} returns

   [0 < m] |- f (a * m = b * m) x <=> f (a = b) x

Likewise, when the goal is {tm} above,
{e (VALIDATE (CONV_TAC (DEPTH_CONV (REWR_CONV_A th))))}
gives the two subgoals:

      f (a = b) x

      0 < m


SEEALSO
Conv.REWR_CONV, Rewrite.REWRITE_CONV, Conv.DEPTH_CONV,
Tactic.CONV_TAC, Tactical.VALIDATE.

----------------------------------------------------------------------