Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-28 02:42:01 -0800 (Wed, 28 Jan 2004)
Revision: 5300
Log message:

      Defined Integral Domain.
      

Changes	Path
+2 -1	metaprl/theories/itt/Makefile
+3 -1	metaprl/theories/itt/OMakefile
+115 -108	metaprl/theories/itt/itt_field2.ml
+4494 -4200	metaprl/theories/itt/itt_field2.prla
+2 -0	metaprl/theories/itt/itt_int_ext.mli
Added	metaprl/theories/itt/itt_intdomain.ml
Properties	metaprl/theories/itt/itt_intdomain.ml
Added	metaprl/theories/itt/itt_intdomain.mli
Properties	metaprl/theories/itt/itt_intdomain.mli
Added	metaprl/theories/itt/itt_intdomain.prla
Properties	metaprl/theories/itt/itt_intdomain.prla
+0 -1	metaprl/theories/itt/itt_ring2.ml
+4271 -4348	metaprl/theories/itt/itt_ring2.prla
+0 -1	metaprl/theories/itt/itt_unitring.ml
+1274 -1254	metaprl/theories/itt/itt_unitring.prla