Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:08:36 -0800 (Tue, 02 Apr 2002)
Revision: 3556
Log message:

      1. Changed the representation of subgroups; it looks more natural now.
      2. Updated the definition of subgroups. Since "eqG" was added to the def.
         of groups, the def. of a subgroup must give the description for "eqG".\
      3. Updated all rules and reproved them.
      
      TODO:
      I just realized that the def. for subgroups are not sufficient yet:
        1. "equiv" instead of "equal" should be used for the operations;
        2. the description for "eqG" is not complete; I should also give
           the other side, i.e., if a and b are in s and a is equivalent
           to b under eqG{g}, then a is also equivalent to b under eqG{s}.
      Will correct these soon.
      

Changes	Path
+28 -34	metaprl/theories/czf/czf_itt_subgroup.ml
+3 -3	metaprl/theories/czf/czf_itt_subgroup.mli
+2562 -2413	metaprl/theories/czf/czf_itt_subgroup.prla