Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-21 11:12:37 -0800 (Tue, 21 Feb 2006)
Revision: 8763
Log message:

      The rule generation code should use second-order variables for the logic.
      
      Added a dummy file Itt_hoas_sequent_elim.
      

Changes  Path
+4 -4 metaprl/OMakefile_theories
+2 -2 metaprl/filter/base/filter_reflection.ml
+0 -1 metaprl/filter/filter/filter_reflect.ml
+1 -0 metaprl/theories/itt/reflection/experimental/MetaprlInfo
Added metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_elim.ml
Properties metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_elim.ml
Added metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_elim.mli
Properties metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_elim.mli
+1 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_theory.mlz