Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-22 19:22:39 -0800 (Mon, 22 Dec 2003)
Revision: 5204
Log message:
1. Itt_grouplikeobj: isMonoid_wf2 added and proved,
I'd say that this form should be in intro-resource
instead of isMonoid_wf
2. itt_record: recordOrtBisectIntro added and proved, recordOrt added to .mli
3. itt_field: a couple of intermediate lemmas added.