Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-10 03:47:25 -0700 (Sat, 10 May 2003)
Revision: 4580
Log message:

      Defined {i..j-1} and {0..j-1} (in order to define finite sets).
      

Changes	Path
+3 -1	metaprl/theories/itt/itt_group.ml
+29 -0	metaprl/theories/itt/itt_int_ext.ml
+3 -0	metaprl/theories/itt/itt_int_ext.mli
+6186 -5902	metaprl/theories/itt/itt_int_ext.prla
+14 -0	metaprl/theories/itt/itt_nat.ml
+1 -0	metaprl/theories/itt/itt_nat.mli
+974 -721	metaprl/theories/itt/itt_nat.prla
+3 -5	metaprl/theories/itt/itt_quotient_group.ml