Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-23 13:51:24 -0700 (Fri, 23 Jul 1999)
Revision: 2805
Log message:

      Some theories still had Itt_squash!squash instead of Base_trivial!squash - fixed.
      Now more old proofs expand correctly.
      

Changes  Path
+37 -40 metaprl/theories/itt/itt_bisect.prla
+56 -62 metaprl/theories/itt/itt_bool.prla
+1 -1 metaprl/theories/itt/itt_bunion.mli
+15 -21 metaprl/theories/itt/itt_bunion.prla
+167 -173 metaprl/theories/itt/itt_collection.prla
+2 -2 metaprl/theories/itt/itt_decidable.prla
+4 -10 metaprl/theories/itt/itt_dprod.prla
+87 -93 metaprl/theories/itt/itt_dprod_imp.prla
+18 -24 metaprl/theories/itt/itt_fun.prla
+16 -22 metaprl/theories/itt/itt_list.prla
+59 -65 metaprl/theories/itt/itt_list2.prla
+10 -16 metaprl/theories/itt/itt_logic.prla
+10 -16 metaprl/theories/itt/itt_prop_decide.prla