Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-25 19:22:16 -0800 (Fri, 25 Nov 2005)
Revision: 8215
Log message:

      Deriving the sequent_ind reight reduction.
      

Changes  Path
+7 -1 metaprl/support/display/perv.ml
+2 -0 metaprl/support/display/perv.mli
Properties metaprl/theories/itt/extensions/vector
Copied metaprl/theories/itt/extensions/vector/OMakefile
Added metaprl/theories/itt/extensions/vector/itt_vec_struct.ml
Properties metaprl/theories/itt/extensions/vector/itt_vec_struct.ml
Added metaprl/theories/itt/extensions/vector/itt_vec_struct.mli
Properties metaprl/theories/itt/extensions/vector/itt_vec_struct.mli
+0 -0 metaprl/theories/meta/base/base_rewrite.ml
+2 -0 metaprl/theories/meta/extensions/OMakefile
+18 -11 metaprl/theories/meta/extensions/meta_context_ind1.ml
+1 -0 metaprl/theories/meta/extensions/meta_context_ind1.mli
Added metaprl/theories/meta/extensions/meta_context_rewrite.ml
Properties metaprl/theories/meta/extensions/meta_context_rewrite.ml
Added metaprl/theories/meta/extensions/meta_context_rewrite.mli
Properties metaprl/theories/meta/extensions/meta_context_rewrite.mli
Added metaprl/theories/meta/extensions/meta_context_rewrite.prla
Properties metaprl/theories/meta/extensions/meta_context_rewrite.prla
+17 -28 metaprl/theories/meta/extensions/meta_context_terms.ml
+14 -0 metaprl/theories/meta/extensions/meta_context_terms.mli
Added metaprl/theories/meta/extensions/meta_rewrite.ml
Properties metaprl/theories/meta/extensions/meta_rewrite.ml
Added metaprl/theories/meta/extensions/meta_rewrite.mli
Properties metaprl/theories/meta/extensions/meta_rewrite.mli