Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-23 23:43:47 -0800 (Sat, 23 Mar 2002)
Revision: 3544
Log message:
Changed the definition of abelian groups completely. An abelian
group is now defined under equivalence relations instead of equality
relations, and there is a reduction rule for it.
Changes | Path |
+34 -13 | metaprl/theories/czf/czf_itt_abel_group.ml |
+25 -1 | metaprl/theories/czf/czf_itt_abel_group.mli |
+851 -303 | metaprl/theories/czf/czf_itt_abel_group.prla |