Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-07 18:14:28 -0800 (Wed, 07 Jan 2004)
Revision: 5235
Log message:

       - Defined subring.
       - Added more ring examples.
      
       Notes:
         1. The typeinf_resource for as_additive needs work.
         2. The ring of even integers is commented out since for now
            we don't have enough axioms for the "rem" operation.
            I would appreciate if Yegor can add it( and incorporate it
            into arithT).
      

Changes	Path
+5 -0	metaprl/theories/itt/itt_group.ml
+174 -6	metaprl/theories/itt/itt_ring2.ml
+7 -0	metaprl/theories/itt/itt_ring2.mli
+13431 -4353	metaprl/theories/itt/itt_ring2.prla