Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-05 23:58:11 -0700 (Wed, 05 Apr 2006)
Revision: 9029
Log message:

      Added support for "vsequent{...} in SequentRelax"; updated the proof in Reflect_pmn_core_logic_test.
      

Changes  Path
+7 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.ml
+1121 -1059 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.prla
+12 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.ml
+3506 -4427 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.prla
+996 -6080 metaprl/theories/poplmark/naive/reflect_pmn_core_logic_test.prla