REWR_CONV_A : (thm -> conv)
STRUCTURE
Conv
SYNOPSIS
Uses an instance of a given equation to rewrite a term.
DESCRIPTION
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
REWR_CONV, REWRITE_CONV, DEPTH_CONV, CONV_TAC, VALIDATE
HOL  Trindemossen-1