Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-07 01:06:43 -0800 (Wed, 07 Feb 2001)
Revision: 3145
Log message:

      Most of rules are proved. Elimination rule fixed and proved.
      

Changes  Path
+16 -2 metaprl/theories/itt/itt_int_base.ml
+16 -2 metaprl/theories/itt/itt_int_base.mli
+2014 -1493 metaprl/theories/itt/itt_int_base.prla