Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-10 19:52:00 -0800 (Fri, 10 Mar 2006)
Revision: 8870
Log message:

      Added the ProofCheck lemmas.
      

Changes  Path
+119 -14 metaprl/filter/base/filter_reflection.ml
+1 -0 metaprl/filter/base/filter_reflection.mli
+21 -10 metaprl/filter/base/filter_util.ml
+1 -0 metaprl/filter/base/filter_util.mli
+45 -37 metaprl/filter/filter/filter_reflect.ml
+2 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_elim.ml
+1 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_elim.mli