Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-03 16:55:20 -0700 (Tue, 03 Jul 2001)
Revision: 3312
Log message:

      - Now substitution (s1=s2 in S) for conclution (t in T[s1]) produces a wf subgoal
         s:S |- T[s] Type
      (instead of s:S |- (t in T[s]) Type which was annoying)
      
      - Now assertEqT is more powerful than it was.
      

Changes	Path
+222 -332	metaprl/theories/itt/itt_disect.prla
+43 -13	metaprl/theories/itt/itt_struct2.ml
+4542 -3371	metaprl/theories/itt/itt_struct2.prla
+0 -2	metaprl/theories/itt/itt_theory.ml