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 |