Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 18:39:29 -0800 (Mon, 03 Mar 2003)
Revision: 4153
Log message:
- Moved "csemigroup"(the set of commutative semigroup) and "cmonoid" to
"itt_grouplikeobj" and "abelg" to "itt_group"
- Added the intro and elim rules for them. For example:
'g in group[i:l] & isCommutative{'g} <=> 'g in abelg[i:l]
- Corrected a typo in the display form of semigroup
I'm not quite sure whether these elimination rules are better or the ones
that completely unfold, say "abelg" are better. I put the second option
in comments for now.