Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-29 13:34:13 -0800 (Thu, 29 Dec 2005)
Revision: 8385
Log message:

      Reformulating the Provable theorems.
      

Changes  Path
+0 -2 metaprl/filter/base/filter_grammar.ml
+154 -130 metaprl/filter/base/filter_reflection.ml
+13 -4 metaprl/filter/base/filter_reflection.mli
+78 -53 metaprl/filter/filter/filter_parse.ml
+9 -0 metaprl/support/display/summary.ml
+18 -7 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.ml
+6 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.mli
+788 -462 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.prla
+1 -1 metaprl/theories/poplmark/naive/pmn_core_terms.ml