Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-02 02:29:52 -0800 (Wed, 02 Apr 2003)
Revision: 4372
Log message:

      Completed all proofs except for "itt_subset/member_doesnot_depend_on_B".
      
      Alexei, can you take a look at this rule? I think the assumptions should
      be subset instead of subtype.
      

Changes  Path
+6 -0 metaprl/theories/itt/itt_grouplikeobj.ml
+1624 -1162 metaprl/theories/itt/itt_grouplikeobj.prla
+825 -867 metaprl/theories/itt/itt_subset.prla