Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 15:37:25 -0700 (Tue, 20 Jun 2006)
Revision: 9350
Log message:

      Added new tactics:
       * reduceForallProdT rewrites hyps of the form all x: A*B*C... as all a:A.all b:B. all c:C...
      
       * varElimT : int -> tactic
       Eliminate a variable x using an equality x=t in A
      
       * allVarElimT
       Eliminate all possible variables.