Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-10 18:46:26 -0800 (Sat, 10 Dec 2005)
Revision: 8273
Log message:

      Proved the suffix part of sequent reduction.
      

Changes  Path
+2 -0 metaprl/refiner/refiner/refiner_debug.ml
+8 -3 metaprl/theories/itt/extensions/base/itt_list3.ml
+1590 -1361 metaprl/theories/itt/extensions/base/itt_list3.prla
+37 -3 metaprl/theories/itt/extensions/vector/itt_vec_bind.ml
+7 -0 metaprl/theories/itt/extensions/vector/itt_vec_bind.mli
+3393 -1841 metaprl/theories/itt/extensions/vector/itt_vec_bind.prla
+254 -26 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term1.ml
+4 -0 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term1.mli
+8814 -1432 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term1.prla