Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-13 15:33:59 -0800 (Mon, 13 Mar 2006)
Revision: 8884
Log message:

      - Changed the SimpleStep definition to use ProofCheck and the ValidStep
        definition to use SimpleStep.
      
      - Proved stronger (dependent) elimination rules for the SimpleStep.
      

Changes  Path
+45 -39 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.ml
+2486 -2500 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.prla
+10 -10 metaprl/theories/itt/reflection/experimental/itt_hoas_proof_ind.ml
+809 -699 metaprl/theories/itt/reflection/experimental/itt_hoas_proof_ind.prla
+191 -200 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_proof.prla
+7609 -3710 metaprl/theories/poplmark/naive/reflect_pmn_core_terms.prla