Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 22:58:44 -0700 (Mon, 08 Apr 2002)
Revision: 3569
Log message:

      Defined "group builder" group_bvd{'h; 'g; 's} which build a group
      h from group g where the underlying set of h is s, the operation
      and equivalence relation in h are the same as in g. The only use
      for the introduction of group_bvd is to make codes cleaner, nicer,
      or easier to understand. (See examples in Czf_itt_subgroup,
      Czf_itt_cyclic_subgroup, and Czf_itt_hom.)
      

Changes	Path
Added	metaprl/theories/czf/czf_itt_group_bvd.ml
Properties	metaprl/theories/czf/czf_itt_group_bvd.ml
Added	metaprl/theories/czf/czf_itt_group_bvd.mli
Properties	metaprl/theories/czf/czf_itt_group_bvd.mli
Added	metaprl/theories/czf/czf_itt_group_bvd.prla
Properties	metaprl/theories/czf/czf_itt_group_bvd.prla