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