Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-27 22:07:21 -0800 (Mon, 27 Mar 2006)
Revision: 8956
Log message:

      More progress on wf theorems.
      

Changes  Path
+51 -0 metaprl/theories/itt/extensions/vector/itt_vec_list1.ml
+1 -0 metaprl/theories/itt/extensions/vector/itt_vec_list1.mli
+2 -2 metaprl/theories/itt/reflection/core/itt_hoas_vbind.ml
+4 -0 metaprl/theories/itt/reflection/core/itt_hoas_vbind.mli
+0 -32 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
+9877 -8695 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla
+4 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_relax.ml
+2 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_relax.mli
+203 -151 metaprl/theories/itt/reflection/experimental/itt_hoas_relax.prla
+5372 -4293 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla
+24 -11 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.ml
+3084 -2958 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.prla