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 |