Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-02 00:19:23 -0800 (Fri, 02 Feb 2001)
Revision: 3133
Log message:

      sqeq2rwT: tactic -> tactic  added. It apply argument and then make all conversions from squash to ext. It is useful to proving rewrites derived from sqequal-rules
      

Changes	Path
+6 -3	metaprl/theories/itt/itt_int_base.ml
+2 -1	metaprl/theories/itt/itt_int_base.mli