Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:18:40 -0800 (Tue, 02 Apr 2002)
Revision: 3557
Log message:
1. Changed the representation of cyclic subgroups; it looks more
natural now.
2. Updated the definition of cyclic subgroups. Since "eqG" was added
to the def. of groups, the def. of a cyclic subgroup must give the
description for "eqG" too.
3. Updated all rules and reproved them.
The same problems as in subgroups exist here also. Will fix soon.
Changes | Path |
+19 -34 | metaprl/theories/czf/czf_itt_cyclic_subgroup.ml |
+3 -4 | metaprl/theories/czf/czf_itt_cyclic_subgroup.mli |
+6524 -2230 | metaprl/theories/czf/czf_itt_cyclic_subgroup.prla |