Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 2000-09-04 10:09:49 -0700 (Mon, 04 Sep 2000)
Revision: 3056
Log message:

      Started changing declare/prim_rw to define (as in TODO 2.01.2).
      Also fixed an unsoundness in itt_dprod.ml where fst{} had two definitions:
      
       prim_rw unfoldFst : fst{'e} <--> spread{'e; u, v. 'u}
       prim_rw unfoldSnd : fst{'e} <--> spread{'e; u, v. 'v}
      

Changes  Path
+2 -6 metaprl/theories/itt/itt_bisect.ml
+2 -3 metaprl/theories/itt/itt_bisect.mli
+9 -18 metaprl/theories/itt/itt_bool.ml
+9 -17 metaprl/theories/itt/itt_bool.mli
+2 -3 metaprl/theories/itt/itt_bunion.ml
+2 -3 metaprl/theories/itt/itt_bunion.mli
+1 -2 metaprl/theories/itt/itt_decidable.ml
+3 -4 metaprl/theories/itt/itt_decidable.mli
+2 -4 metaprl/theories/itt/itt_dprod.ml
+2 -4 metaprl/theories/itt/itt_dprod.mli
+10 -20 metaprl/theories/itt/itt_dprod_imp.ml
+6 -8 metaprl/theories/itt/itt_esquash.ml
+1 -2 metaprl/theories/itt/itt_ext_equal.ml
+3 -6 metaprl/theories/itt/itt_int.ml
+3 -6 metaprl/theories/itt/itt_int.mli
+35 -46 metaprl/theories/itt/itt_list2.ml
+1 -1 metaprl/theories/itt/itt_list2.mli
+12 -24 metaprl/theories/itt/itt_logic.ml
+11 -26 metaprl/theories/itt/itt_sort.ml
+2 -2 metaprl/theories/itt/itt_sort.mli
+1 -2 metaprl/theories/itt/itt_test.ml
+9 -14 metaprl/theories/itt/itt_well_founded.ml