Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-05 18:40:38 -0800 (Mon, 05 Dec 2005)
Revision: 8266
Log message:

      Intermediate commit while considering strategy sugeessted by Aleksey.
      

Changes  Path
+2 -2 metaprl/refiner/term_ds/term_subst_ds.ml
+65 -1 metaprl/theories/itt/extensions/base/itt_list3.ml
+18 -0 metaprl/theories/itt/extensions/base/itt_list3.mli
+2276 -606 metaprl/theories/itt/extensions/base/itt_list3.prla
+176 -0 metaprl/theories/itt/extensions/vector/itt_vec_bind.ml
+17 -0 metaprl/theories/itt/extensions/vector/itt_vec_bind.mli
+4549 -199 metaprl/theories/itt/extensions/vector/itt_vec_bind.prla
+92 -93 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term.ml
+9770 -2316 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term.prla