Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-13 19:19:35 -0700 (Sun, 13 Jun 1999)
Revision: 2710
Log message:
Added equalityEquality to the eqcd resource, so eqcdT and dT 0 can handle
<< ('a1 = 'b1 in 'T1) = ('a2 = 'b2 in 'T2) in univ[i:l] >>.
Updated documentation.
Changes | Path |
+12 -4 | metaprl/doc/itt_quickref.txt |
+3 -0 | metaprl/theories/itt/itt_equal.ml |