Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 01:55:08 -0700 (Wed, 09 Jun 2004)
Revision: 5867
Log message:

      The Itt_dprod.productSubtype rule was invalid! I've added the missing wf
      assumption and turned the rule from an invalid prim to a proven
      interactive one.
      

Changes	Path
+6 -6	metaprl/theories/itt/itt_dprod.ml
+0 -11	metaprl/theories/itt/itt_dprod.mli
+1960 -1834	metaprl/theories/itt/itt_dprod.prla
+963 -1354	metaprl/theories/itt/itt_prod.prla