Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-24 00:26:30 -0800 (Sun, 24 Mar 2002)
Revision: 3547
Log message:

      Defined homomorphism for groups. A map f of a group G into a group G'
      is a homomorphism if f(a * b) = f(a) * f(b).
      
      Proved some properties of homomorphism with the definition.
      
      Since I would redo groups soon, this homomorphism file is not complete.
      

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