Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-18 19:44:19 -0800 (Mon, 18 Feb 2002)
Revision: 3501
Log message:

      Changed the definition of subgroups to subgroup{'g; 's} where 'g, 's,
      and subgroup{'g; 's} are all labels.
      Proved the properties of subgroups with this definition.
      
      TODO:
         I would adopt another definition of subgroups where 's is a "set"
         and subgroup{'g; 's} is a "type".
      

Changes	Path
+66 -47	metaprl/theories/czf/czf_itt_subgroup.ml
+1 -1	metaprl/theories/czf/czf_itt_subgroup.mli
+1471 -1535	metaprl/theories/czf/czf_itt_subgroup.prla