Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-05 00:20:00 -0800 (Tue, 05 Feb 2002)
Revision: 3491
Log message:
Proved all rules related to the properties of cyclic subgroups.
TODO:
rule lt_Id and tactic lt_IdT are better to be moved into module "itt_int_base" upon Yegor's approval.
Changes | Path |
+7 -0 | metaprl/theories/czf/czf_itt_cyclic_subgroup.ml |
+5 -0 | metaprl/theories/czf/czf_itt_cyclic_subgroup.mli |
+1883 -714 | metaprl/theories/czf/czf_itt_cyclic_subgroup.prla |