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 |