Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:08:36 -0800 (Tue, 02 Apr 2002)
Revision: 3556
Log message:
1. Changed the representation of subgroups; it looks more natural now.
2. Updated the definition of subgroups. Since "eqG" was added to the def.
of groups, the def. of a subgroup must give the description for "eqG".\
3. Updated all rules and reproved them.
TODO:
I just realized that the def. for subgroups are not sufficient yet:
1. "equiv" instead of "equal" should be used for the operations;
2. the description for "eqG" is not complete; I should also give
the other side, i.e., if a and b are in s and a is equivalent
to b under eqG{g}, then a is also equivalent to b under eqG{s}.
Will correct these soon.
Changes | Path |
+28 -34 | metaprl/theories/czf/czf_itt_subgroup.ml |
+3 -3 | metaprl/theories/czf/czf_itt_subgroup.mli |
+2562 -2413 | metaprl/theories/czf/czf_itt_subgroup.prla |