Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-29 15:30:58 -0800 (Wed, 29 Mar 2006)
Revision: 8962
Log message:

      Finally proved the lemmas about SubLogic.
      

Changes  Path
+10 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.ml
+2405 -1369 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.prla
+7 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_proof_ind.ml
+372 -67 metaprl/theories/itt/reflection/experimental/itt_hoas_proof_ind.prla