Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 20:13:33 -0800 (Sun, 12 Feb 2006)
Revision: 8670
Log message:

      Reverted revisions 8657, 8659, and 8660. These revisions have made the
      elimination rule for the image type stronger than what is valid under pairwise
      functionality and used those invalid rules to derive the itt_list theory.
      

Changes  Path
+18 -17 metaprl/theories/itt/core/itt_bunion.ml
+1942 -1925 metaprl/theories/itt/core/itt_bunion.prla
+25 -28 metaprl/theories/itt/core/itt_image.ml
+3 -3 metaprl/theories/itt/core/itt_image.mli
+2709 -2805 metaprl/theories/itt/core/itt_image.prla
+46 -55 metaprl/theories/itt/core/itt_list.ml
+1 -1 metaprl/theories/itt/core/itt_list.mli
+4086 -5658 metaprl/theories/itt/core/itt_list.prla
+1 -0 metaprl/theories/itt/core/itt_list2.ml
+21209 -12920 metaprl/theories/itt/core/itt_list2.prla
+1 -4 metaprl/theories/itt/core/itt_squash.ml
+1067 -990 metaprl/theories/itt/core/itt_subset2.prla
+24 -27 metaprl/theories/itt/core/itt_tunion.ml
+42 -6 metaprl/theories/itt/core/itt_tunion.mli
+2624 -2989 metaprl/theories/itt/core/itt_tunion.prla
+5697 -2567 metaprl/theories/itt/extensions/base/itt_list_sloppy.prla
+3326 -2663 metaprl/theories/itt/reflection/core/itt_hoas_debruijn.prla
+6 -7 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm.ml
+6304 -6494 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm.prla
+14 -15 metaprl/theories/itt/reflection/experimental/itt_hoas_lang.ml
+5013 -5168 metaprl/theories/itt/reflection/experimental/itt_hoas_lang.prla