Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-02 03:40:19 -0700 (Fri, 02 May 2003)
Revision: 4543
Log message:

      Defined quotient group.
      Added universe equality for mem, subset, and member.
      

Changes	Path
+1 -0	metaprl/theories/itt/Makefile
+4 -4	metaprl/theories/itt/itt_group.ml
+1423 -1530	metaprl/theories/itt/itt_group.prla
Added	metaprl/theories/itt/itt_quotient_group.ml
Properties	metaprl/theories/itt/itt_quotient_group.ml
Added	metaprl/theories/itt/itt_quotient_group.mli
Properties	metaprl/theories/itt/itt_quotient_group.mli
Added	metaprl/theories/itt/itt_quotient_group.prla
Properties	metaprl/theories/itt/itt_quotient_group.prla
+7 -0	metaprl/theories/itt/itt_singleton.ml
+750 -705	metaprl/theories/itt/itt_singleton.prla
+21 -1	metaprl/theories/itt/itt_subset.ml
+1 -1	metaprl/theories/itt/itt_subset.mli
+1814 -1430	metaprl/theories/itt/itt_subset.prla