Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-22 20:46:49 -0700 (Sun, 22 Jul 2001)
Revision: 3346
Log message:

      Added subtypeT function:
      subtypeT <<A>> replaces a conclusion of the form <<t1 = t2 in B>> with
      <<t1 = t2 in A>> and conclusion of any other form <<B>> with just
      <<A>> and generates an "aux" subgoal of the form <<subtype{A;B}>>.
      

Changes  Path
+8 -12 metaprl/doc/itt_quickref.txt
+2 -2 metaprl/theories/itt/itt_dfun.ml
+2 -2 metaprl/theories/itt/itt_dfun.mli
+2305 -2776 metaprl/theories/itt/itt_fun.prla
+18 -1 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_subtype.mli
Added metaprl/theories/itt/itt_subtype.prla
Properties metaprl/theories/itt/itt_subtype.prla