Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-01 23:45:26 -0800 (Mon, 01 Apr 2002)
Revision: 3553
Log message:
1. Added "eqG" to the definition of groups which denotes the equivalence
relation related with the group. Every group has an equivalence
relation, which is now explicitly described.
2. Accordingly, all rules related with equivalence relations in groups
are updated and reproved.
3. Added tactics "uniqueInvLeftT" and "uniqueInvRightT" which might not
be very useful though.
Changes | Path |
+121 -132 | metaprl/theories/czf/czf_itt_group.ml |
+11 -6 | metaprl/theories/czf/czf_itt_group.mli |
+5698 -5156 | metaprl/theories/czf/czf_itt_group.prla |