Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-05 23:26:04 -0700 (Sat, 05 Jun 1999)
Revision: 2691
Log message:
Added a new primitive rule universeCumulativity and corresponding
tactic cumulativityT.
| Changes | Path |
| +4 -0 | metaprl/doc/itt_quickref.txt |
| +19 -0 | metaprl/theories/itt/itt_equal.ml |
| +1 -0 | metaprl/theories/itt/itt_equal.mli |