Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-29 00:22:39 -0800 (Thu, 29 Jan 2004)
Revision: 5312
Log message:

      Defined ring, commutative unitring, integral domain, and field with
      decidable equality.
      

Changes	Path
+6 -2	metaprl/theories/itt/Makefile
+10 -2	metaprl/theories/itt/OMakefile
Added	metaprl/theories/itt/itt_fieldE.ml
Properties	metaprl/theories/itt/itt_fieldE.ml
Added	metaprl/theories/itt/itt_fieldE.mli
Properties	metaprl/theories/itt/itt_fieldE.mli
Added	metaprl/theories/itt/itt_fieldE.prla
Properties	metaprl/theories/itt/itt_fieldE.prla
+1 -1	metaprl/theories/itt/itt_intdomain.ml
Added	metaprl/theories/itt/itt_intdomainE.ml
Properties	metaprl/theories/itt/itt_intdomainE.ml
Added	metaprl/theories/itt/itt_intdomainE.mli
Properties	metaprl/theories/itt/itt_intdomainE.mli
Added	metaprl/theories/itt/itt_intdomainE.prla
Properties	metaprl/theories/itt/itt_intdomainE.prla
+5 -145	metaprl/theories/itt/itt_poly.ml
+1 -16	metaprl/theories/itt/itt_poly.mli
Added	metaprl/theories/itt/itt_ringE.ml
Properties	metaprl/theories/itt/itt_ringE.ml
Added	metaprl/theories/itt/itt_ringE.mli
Properties	metaprl/theories/itt/itt_ringE.mli
Added	metaprl/theories/itt/itt_ringE.prla
Properties	metaprl/theories/itt/itt_ringE.prla
+1 -1	metaprl/theories/itt/itt_unitring.ml
Added	metaprl/theories/itt/itt_unitringCE.ml
Properties	metaprl/theories/itt/itt_unitringCE.ml
Added	metaprl/theories/itt/itt_unitringCE.prla
Properties	metaprl/theories/itt/itt_unitringCE.prla