Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-23 15:12:44 -0700 (Tue, 23 Jun 1998)
Revision: 2272
Log message:

      Improved rewriter speed with conversion tree and flist.
      

Changes	Path
+5 -2	metaprl/editor/ml/shell_rule.ml
+15 -2	metaprl/editor/ml/y.ml
+5 -3	metaprl/filter/filter_prog.ml
+2 -1	metaprl/mllib/Makefile
Added	metaprl/mllib/flist.ml
Properties	metaprl/mllib/flist.ml
Added	metaprl/mllib/flist.mli
Properties	metaprl/mllib/flist.mli
+7 -0	metaprl/refiner/refiner/refine.ml
+73 -26	metaprl/refiner/refiner/rewrite.ml
+13 -1	metaprl/refiner/term_ds/term_subst_ds.ml
Properties	metaprl/theories/czf
+8 -1	metaprl/theories/czf/Makefile
Added	metaprl/theories/czf/czf_itt_all.ml
Properties	metaprl/theories/czf/czf_itt_all.ml
Added	metaprl/theories/czf/czf_itt_all.mli
Properties	metaprl/theories/czf/czf_itt_all.mli
Added	metaprl/theories/czf/czf_itt_and.ml
Properties	metaprl/theories/czf/czf_itt_and.ml
Added	metaprl/theories/czf/czf_itt_and.mli
Properties	metaprl/theories/czf/czf_itt_and.mli
Added	metaprl/theories/czf/czf_itt_axioms.ml
Properties	metaprl/theories/czf/czf_itt_axioms.ml
Added	metaprl/theories/czf/czf_itt_axioms.mli
Properties	metaprl/theories/czf/czf_itt_axioms.mli
Added	metaprl/theories/czf/czf_itt_dall.ml
Properties	metaprl/theories/czf/czf_itt_dall.ml
Added	metaprl/theories/czf/czf_itt_dall.mli
Properties	metaprl/theories/czf/czf_itt_dall.mli
Added	metaprl/theories/czf/czf_itt_dexists.ml
Properties	metaprl/theories/czf/czf_itt_dexists.ml
Added	metaprl/theories/czf/czf_itt_dexists.mli
Properties	metaprl/theories/czf/czf_itt_dexists.mli
Added	metaprl/theories/czf/czf_itt_exists.ml
Properties	metaprl/theories/czf/czf_itt_exists.ml
Added	metaprl/theories/czf/czf_itt_exists.mli
Properties	metaprl/theories/czf/czf_itt_exists.mli
Added	metaprl/theories/czf/czf_itt_implies.ml
Properties	metaprl/theories/czf/czf_itt_implies.ml
Added	metaprl/theories/czf/czf_itt_implies.mli
Properties	metaprl/theories/czf/czf_itt_implies.mli
+7 -0	metaprl/theories/czf/czf_itt_or.ml
+7 -0	metaprl/theories/czf/czf_itt_or.mli
+73 -6	metaprl/theories/czf/czf_itt_set.ml
+47 -6	metaprl/theories/czf/czf_itt_set.mli
+2 -2	metaprl/theories/itt/Makefile
+7 -4	metaprl/theories/itt/itt_dfun.ml
+6 -3	metaprl/theories/itt/itt_dfun.mli
+13 -14	metaprl/theories/itt/itt_dprod.ml
+5 -2	metaprl/theories/itt/itt_dprod.mli
+4 -1	metaprl/theories/itt/itt_fun.ml
+11 -8	metaprl/theories/itt/itt_logic.ml
+6 -6	metaprl/theories/itt/itt_prod.ml
+5 -2	metaprl/theories/itt/itt_rfun.ml
+8 -5	metaprl/theories/itt/itt_struct.ml
+4 -2	metaprl/theories/itt/itt_test.ml
+73 -44	metaprl/theories/tactic/conversionals.ml
+5 -0	metaprl/theories/tactic/conversionals.mli
+148 -35	metaprl/theories/tactic/rewrite_type.ml
+12 -2	metaprl/theories/tactic/rewrite_type.mli
+74 -97	metaprl/theories/tactic/tactic_type.ml