Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-17 17:27:19 -0800 (Mon, 17 Jan 2005)
Revision: 6426
Log message:

      This extends the term classification system.
      

Changes	Path
+162 -152	metaprl-branches/opname_classes/filter/base/filter_cache_fun.ml
+1 -1	metaprl-branches/opname_classes/filter/base/filter_magic.ml
+287 -154	metaprl-branches/opname_classes/filter/base/filter_summary.ml
+5 -4	metaprl-branches/opname_classes/filter/base/filter_summary_type.ml
+23 -9	metaprl-branches/opname_classes/filter/base/filter_type.ml
+77 -82	metaprl-branches/opname_classes/filter/filter/filter_parse.ml
+33 -17	metaprl-branches/opname_classes/filter/filter/filter_prog.ml
+278 -65	metaprl-branches/opname_classes/filter/filter/term_grammar.ml
+1 -0	metaprl-branches/opname_classes/refiner/refiner/refiner_ds.ml
+1 -0	metaprl-branches/opname_classes/refiner/refiner/refiner_std.ml
+1 -0	metaprl-branches/opname_classes/refiner/refsig/Files
+3 -0	metaprl-branches/opname_classes/refiner/refsig/refiner_sig.ml
Added	metaprl-branches/opname_classes/refiner/refsig/term_class_sig.ml
Properties	metaprl-branches/opname_classes/refiner/refsig/term_class_sig.ml
+1 -0	metaprl-branches/opname_classes/refiner/term_gen/Files
Added	metaprl-branches/opname_classes/refiner/term_gen/term_class_gen.ml
Properties	metaprl-branches/opname_classes/refiner/term_gen/term_class_gen.ml
Added	metaprl-branches/opname_classes/refiner/term_gen/term_class_gen.mli
Properties	metaprl-branches/opname_classes/refiner/term_gen/term_class_gen.mli
+1 -0	metaprl-branches/opname_classes/refiner/term_gen/term_shape_gen.ml
+4 -4	metaprl-branches/opname_classes/support/shell/shell_core.ml
+4 -4	metaprl-branches/opname_classes/support/shell/shell_package.ml
+1 -0	metaprl-branches/opname_classes/support/shell/shell_state.ml
+4 -7	metaprl-branches/opname_classes/theories/experimental/syntax/syntax_test.ml
+0 -1	metaprl-branches/opname_classes/theories/experimental/syntax/syntax_test.mli