Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-06 12:27:51 -0800 (Sat, 06 Dec 2003)
Revision: 5151
Log message:
1.Renaming: rename_mul_add/rename_add_mul/as_additive were not delcared in .mli
2.There was only theorem that G^car is type for groups, added for monoids
3.Basic facts about rings. Additive group defined using renaming (see morph discussion),
elimination rules still have to be fixed.