Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-28 03:25:05 -0700 (Wed, 28 May 2003)
Revision: 4627
Log message:

      - Moved the "top" type declaration from Itt_void (where it resided
      for hackish reasons) to Itt_isect, where it belongs.
      
      - The rule /itt_isect/intersectionSubtype was not valid. Made it weaker
      and derived it.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_dprod.ml
+5 -4 metaprl/theories/itt/itt_isect.ml
+2 -8 metaprl/theories/itt/itt_isect.mli
+4906 -5117 metaprl/theories/itt/itt_isect.prla
+2 -1 metaprl/theories/itt/itt_record.prla
+2 -1 metaprl/theories/itt/itt_record0.prla
+2 -2 metaprl/theories/itt/itt_rfun.ml
+2 -1 metaprl/theories/itt/itt_sortedtree.prla
+2 -1 metaprl/theories/itt/itt_subset.prla
+1 -1 metaprl/theories/itt/itt_subset2.prla
+2 -1 metaprl/theories/itt/itt_tsquash.prla
+1 -1 metaprl/theories/itt/itt_union.ml
+3 -2 metaprl/theories/itt/itt_void.ml
+1 -1 metaprl/theories/itt/itt_void.mli
+2 -1 metaprl/theories/itt/itt_void.prla