Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 01:58:58 -0800 (Mon, 11 Mar 2002)
Revision: 3536
Log message:

      1. Changed the definition of subgroup{'g; 's}; 's is now a "label"
         instead of a "set". In the previous version, it is really hard to
         show that a subgroup is also a group. Now subgroup{'g; 's} is a
         subgroup iff 'g is a group, 's is a group, the carrier set of 's
         is a subset of that of 'g, and they have the same operators;
      2. Rules updated and proved;
      3. Added tactic "subgroupIsectT".
      

Changes	Path
+54 -67	metaprl/theories/czf/czf_itt_subgroup.ml
+13 -0	metaprl/theories/czf/czf_itt_subgroup.mli
+3285 -2630	metaprl/theories/czf/czf_itt_subgroup.prla