Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 23:02:28 -0700 (Mon, 08 Apr 2002)
Revision: 3574
Log message:

      1. Defined group isomorphisms based on group homomorphisms. An
         isomorphism f: G1 -> G2 is a homomorphism that is one-to-one
         and onto G2. That is, an isomorphism f: G1 -> G2 is a
         homomorphism where f is a bijection.
      2. Also defined and proved the functionality rules (both equality
         and equivalence) for isomorphisms.
      

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