Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-15 21:55:45 -0800 (Mon, 15 Dec 2003)
Revision: 5178
Log message:

      1.itt_ring - proved all theorems.
      
      2.itt_record - added a theorem on how recordOrt interplays with set.
      
      3.itt_field - original form of isField was incorrect, finally I added
      [i:l] to it because I say that car0 is equal to certain set.
      Still proof of isField_wf is incomplete yet and huge (it possibly
      means that itt_group*, itt_record* and itt_ring have imperfect design).
      

Changes  Path
+19 -11 metaprl/theories/itt/itt_field.ml
+1 -1 metaprl/theories/itt/itt_field.mli
Added metaprl/theories/itt/itt_field.prla
Properties metaprl/theories/itt/itt_field.prla
+6 -0 metaprl/theories/itt/itt_record.ml
+1358 -1342 metaprl/theories/itt/itt_record.prla
+27 -9 metaprl/theories/itt/itt_ring.ml
+2952 -1814 metaprl/theories/itt/itt_ring.prla