Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-20 23:56:36 -0800 (Wed, 20 Feb 2002)
Revision: 3504
Log message:

      Redefined subgroups. Now subgroup{'g; 's} is a "type" where 's is the
      underlying set for the subgroup and it is no longer defined by axioms,
      but by introduction and elimination rules which make the descriptions
      and proving of subgroup-related properties more straight-forward.
      

Changes	Path
+80 -63	metaprl/theories/czf/czf_itt_subgroup.ml
+2235 -972	metaprl/theories/czf/czf_itt_subgroup.prla