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 |