Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-11 03:57:52 -0700 (Sat, 11 May 2002)
Revision: 3623
Log message:

      Finished the comment part.
      

Changes	Path
+93 -3	metaprl/theories/czf/czf_itt_abel_group.ml
+44 -3	metaprl/theories/czf/czf_itt_abel_group.mli
+2440 -431	metaprl/theories/czf/czf_itt_abel_group.prla
+125 -2	metaprl/theories/czf/czf_itt_cyclic_group.ml
+50 -0	metaprl/theories/czf/czf_itt_cyclic_group.mli
+3277 -596	metaprl/theories/czf/czf_itt_cyclic_group.prla
+159 -10	metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+51 -2	metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+4148 -760	metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+310 -74	metaprl/theories/czf/czf_itt_equiv.ml
+42 -5	metaprl/theories/czf/czf_itt_equiv.mli
+9377 -4275	metaprl/theories/czf/czf_itt_equiv.prla
+219 -19	metaprl/theories/czf/czf_itt_group.ml
+56 -6	metaprl/theories/czf/czf_itt_group.mli
+6453 -1681	metaprl/theories/czf/czf_itt_group.prla
+105 -5	metaprl/theories/czf/czf_itt_group_bvd.ml
+44 -0	metaprl/theories/czf/czf_itt_group_bvd.mli
+3138 -317	metaprl/theories/czf/czf_itt_group_bvd.prla
+214 -28	metaprl/theories/czf/czf_itt_hom.ml
+59 -0	metaprl/theories/czf/czf_itt_hom.mli
+5260 -751	metaprl/theories/czf/czf_itt_hom.prla
+104 -1	metaprl/theories/czf/czf_itt_inv_image.ml
+46 -2	metaprl/theories/czf/czf_itt_inv_image.mli
+2809 -377	metaprl/theories/czf/czf_itt_inv_image.prla
+91 -15	metaprl/theories/czf/czf_itt_iso.ml
+44 -5	metaprl/theories/czf/czf_itt_iso.mli
+2398 -366	metaprl/theories/czf/czf_itt_iso.prla
+115 -2	metaprl/theories/czf/czf_itt_set_bvd.ml
+44 -0	metaprl/theories/czf/czf_itt_set_bvd.mli
+3169 -391	metaprl/theories/czf/czf_itt_set_bvd.prla
+146 -12	metaprl/theories/czf/czf_itt_subgroup.ml
+52 -1	metaprl/theories/czf/czf_itt_subgroup.mli
+3846 -572	metaprl/theories/czf/czf_itt_subgroup.prla