Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-01 03:33:12 -0800 (Thu, 01 Feb 2001)
Revision: 3127
Log message:

      finishSq2ExT: term->int->tactic added.
      It helps to complete prove of rewrites derived from ~-rules
      

Changes	Path
+3 -1	metaprl/theories/itt/itt_int_base.ml
+4 -0	metaprl/theories/itt/itt_int_base.mli