Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-22 22:48:04 -0800 (Mon, 22 Dec 2003)
Revision: 5205
Log message:

      1.itt_subtype: transitivity of subtype stated and proved
      
      2.itt_record: recordOrtSetIntro - needless assumption removed
      
      3.itt_group: isCommutativity_wf add&proved though it's shaded by something else
      
      4.itt_ring: stronger introduction rules proved for AGroup and AAbelG
      
      5.itt_field: isField_wf is complete modulo invOrtRing and car0OrtRing which
      are complete modulo some problems with renaming
      

Changes  Path
+0 -2 metaprl/theories/itt/itt_field.ml
+8 -0 metaprl/theories/itt/itt_field.mli
+1865 -16016 metaprl/theories/itt/itt_field.prla
+54 -109 metaprl/theories/itt/itt_group.ml
+8317 -9214 metaprl/theories/itt/itt_group.prla
+0 -1 metaprl/theories/itt/itt_record.ml
+866 -799 metaprl/theories/itt/itt_record.prla
+6 -0 metaprl/theories/itt/itt_ring.ml
+1334 -1217 metaprl/theories/itt/itt_ring.prla
+14 -28 metaprl/theories/itt/itt_subtype.ml
+2697 -2841 metaprl/theories/itt/itt_subtype.prla