Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-02-18 09:31:21 -0800 (Fri, 18 Feb 2005)
Revision: 6719
Log message:

      All proofs needed for omegaT are ground now.
      There is one weird thing though - only (!) one test in itt_int_bench
      shows dependency on itt_ring2
      omegaT does not depends on ring2
      Itt_int_bench depends on supinf which depends on ring2 which
      makes resources from there available but why only one test has dependency?
      

Changes	Path
+6 -0	metaprl/theories/itt/itt_int_arith.mli
+798 -472	metaprl/theories/itt/itt_int_arith.prla
+49 -47	metaprl/theories/itt/itt_omega.ml
+2 -0	metaprl/theories/itt/itt_omega.mli