Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-14 08:44:03 -0700 (Tue, 14 Jul 1998)
Revision: 2325
Log message:

      Intermediate version with auto tactic.
      

Changes	Path
+1 -0	metaprl/clib/Makefile
+1 -0	metaprl/editor/ml/Makefile
+1 -1	metaprl/editor/ml/io_proof.ml
+25 -11	metaprl/editor/ml/package_df.ml
+1 -6	metaprl/editor/ml/package_df.mli
+5 -1	metaprl/editor/ml/package_info.ml
+1 -0	metaprl/editor/ml/package_type.mlz
+1 -1	metaprl/editor/ml/proof.ml
+1 -1	metaprl/editor/ml/shell_rewrite.ml
+1 -1	metaprl/editor/ml/shell_rule.ml
+14 -19	metaprl/editor/ml/y.ml
+19 -18	metaprl/filter/Makefile
+1 -1	metaprl/filter/filter_cache.ml
+6 -6	metaprl/filter/filter_cache_fun.ml
+10 -8	metaprl/filter/filter_hash.ml
+46 -19	metaprl/filter/filter_ocaml.ml
+25 -8	metaprl/filter/filter_ocaml.mli
+3 -5	metaprl/filter/filter_parse.ml
+1 -1	metaprl/filter/filter_prog.ml
+6 -6	metaprl/filter/filter_summary_io.ml
+5 -5	metaprl/filter/filter_summary_type.mlz
+10 -8	metaprl/filter/mLast_util.ml
+1 -0	metaprl/horus/Makefile
+1 -0	metaprl/library/Makefile
+8 -11	metaprl/mk/config
+2 -0	metaprl/mllib/Makefile
+30 -15	metaprl/mllib/file_base.ml
+5 -5	metaprl/mllib/file_base_type.ml
+5 -4	metaprl/mllib/imp_dag.ml
+1 -0	metaprl/refiner/Makefile
+1 -0	metaprl/refiner/refbase/Makefile
+1 -0	metaprl/refiner/refiner/Makefile
+43 -0	metaprl/refiner/refiner/rewrite.mlp
+1 -0	metaprl/refiner/reflib/Makefile
+12 -0	metaprl/refiner/reflib/dform.ml
+2 -1	metaprl/refiner/reflib/resource.ml
+2 -1	metaprl/refiner/reflib/resource.mli
+3 -1	metaprl/refiner/reflib/simple_print.ml
+1 -0	metaprl/refiner/refsig/Makefile
+6 -0	metaprl/refiner/refsig/term_subst_sig.ml
+1 -0	metaprl/refiner/term_ds/Makefile
+179 -122	metaprl/refiner/term_ds/term_subst_ds.mlp
+1 -0	metaprl/refiner/term_gen/Makefile
+1 -0	metaprl/refiner/term_std/Makefile
+116 -69	metaprl/refiner/term_std/term_subst_std.mlp
+2 -0	metaprl/theories/base/Makefile
Added	metaprl/theories/base/base_auto_tactic.ml
Properties	metaprl/theories/base/base_auto_tactic.ml
Added	metaprl/theories/base/base_auto_tactic.mli
Properties	metaprl/theories/base/base_auto_tactic.mli
+8 -3	metaprl/theories/base/base_cache.ml
+25 -3	metaprl/theories/base/base_dtactic.ml
+7 -0	metaprl/theories/base/base_dtactic.mli
+1 -0	metaprl/theories/base/base_theory.mlz
+1 -1	metaprl/theories/base/nuprl_font.ml
+4 -4	metaprl/theories/base/summary.ml
+33 -9	metaprl/theories/base/typeinf.ml
+1 -0	metaprl/theories/base/typeinf.mli
+4 -9	metaprl/theories/czf/Makefile
+91 -73	metaprl/theories/czf/czf_itt_all.ml
+41 -34	metaprl/theories/czf/czf_itt_all.mli
Binary	metaprl/theories/czf/czf_itt_all.prlb
Properties	metaprl/theories/czf/czf_itt_all.prlb
+54 -92	metaprl/theories/czf/czf_itt_and.ml
+26 -55	metaprl/theories/czf/czf_itt_and.mli
Binary	metaprl/theories/czf/czf_itt_and.prlb
Properties	metaprl/theories/czf/czf_itt_and.prlb
+9 -7	metaprl/theories/czf/czf_itt_dall.ml
+7 -5	metaprl/theories/czf/czf_itt_dall.mli
Binary	metaprl/theories/czf/czf_itt_dall.prlb
Properties	metaprl/theories/czf/czf_itt_dall.prlb
+83 -38	metaprl/theories/czf/czf_itt_dexists.ml
+58 -26	metaprl/theories/czf/czf_itt_dexists.mli
Binary	metaprl/theories/czf/czf_itt_dexists.prlb
Properties	metaprl/theories/czf/czf_itt_dexists.prlb
Binary	metaprl/theories/czf/czf_itt_empty.prlb
Properties	metaprl/theories/czf/czf_itt_empty.prlb
Added	metaprl/theories/czf/czf_itt_eq.ml
Properties	metaprl/theories/czf/czf_itt_eq.ml
Added	metaprl/theories/czf/czf_itt_eq.mli
Properties	metaprl/theories/czf/czf_itt_eq.mli
Binary	metaprl/theories/czf/czf_itt_eq.prlb
Properties	metaprl/theories/czf/czf_itt_eq.prlb
+33 -51	metaprl/theories/czf/czf_itt_false.ml
+10 -19	metaprl/theories/czf/czf_itt_false.mli
Binary	metaprl/theories/czf/czf_itt_false.prlb
Properties	metaprl/theories/czf/czf_itt_false.prlb
+77 -153	metaprl/theories/czf/czf_itt_implies.ml
+38 -87	metaprl/theories/czf/czf_itt_implies.mli
Binary	metaprl/theories/czf/czf_itt_implies.prlb
Properties	metaprl/theories/czf/czf_itt_implies.prlb
Added	metaprl/theories/czf/czf_itt_isect.mli
Properties	metaprl/theories/czf/czf_itt_isect.mli
Added	metaprl/theories/czf/czf_itt_member.ml
Properties	metaprl/theories/czf/czf_itt_member.ml
Added	metaprl/theories/czf/czf_itt_member.mli
Properties	metaprl/theories/czf/czf_itt_member.mli
Binary	metaprl/theories/czf/czf_itt_member.prlb
Properties	metaprl/theories/czf/czf_itt_member.prlb
+65 -98	metaprl/theories/czf/czf_itt_or.ml
+25 -57	metaprl/theories/czf/czf_itt_or.mli
Binary	metaprl/theories/czf/czf_itt_or.prlb
Properties	metaprl/theories/czf/czf_itt_or.prlb
Added	metaprl/theories/czf/czf_itt_res.ml
Properties	metaprl/theories/czf/czf_itt_res.ml
Added	metaprl/theories/czf/czf_itt_res.mli
Properties	metaprl/theories/czf/czf_itt_res.mli
Added	metaprl/theories/czf/czf_itt_sall.ml
Properties	metaprl/theories/czf/czf_itt_sall.ml
Added	metaprl/theories/czf/czf_itt_sall.mli
Properties	metaprl/theories/czf/czf_itt_sall.mli
+43 -9	metaprl/theories/czf/czf_itt_sep.ml
+27 -7	metaprl/theories/czf/czf_itt_sep.mli
Binary	metaprl/theories/czf/czf_itt_sep.prlb
Properties	metaprl/theories/czf/czf_itt_sep.prlb
+135 -183	metaprl/theories/czf/czf_itt_set.ml
+46 -106	metaprl/theories/czf/czf_itt_set.mli
Binary	metaprl/theories/czf/czf_itt_set.prlb
Properties	metaprl/theories/czf/czf_itt_set.prlb
Added	metaprl/theories/czf/czf_itt_sexists.ml
Properties	metaprl/theories/czf/czf_itt_sexists.ml
Added	metaprl/theories/czf/czf_itt_sexists.mli
Properties	metaprl/theories/czf/czf_itt_sexists.mli
Binary	metaprl/theories/czf/czf_itt_small.prlb
Properties	metaprl/theories/czf/czf_itt_small.prlb
+36 -48	metaprl/theories/czf/czf_itt_true.ml
+11 -21	metaprl/theories/czf/czf_itt_true.mli
Binary	metaprl/theories/czf/czf_itt_true.prlb
Properties	metaprl/theories/czf/czf_itt_true.prlb
Binary	metaprl/theories/czf/czf_itt_union.prlb
Properties	metaprl/theories/czf/czf_itt_union.prlb
+2 -0	metaprl/theories/itt/Makefile
Added	metaprl/theories/itt/itt_derive.ml
Properties	metaprl/theories/itt/itt_derive.ml
Added	metaprl/theories/itt/itt_derive.mli
Properties	metaprl/theories/itt/itt_derive.mli
Binary	metaprl/theories/itt/itt_derive.prlb
Properties	metaprl/theories/itt/itt_derive.prlb
+5 -2	metaprl/theories/itt/itt_dfun.ml
+1 -1	metaprl/theories/itt/itt_dprod.ml
+66 -7	metaprl/theories/itt/itt_equal.ml
+18 -0	metaprl/theories/itt/itt_equal.mli
Binary	metaprl/theories/itt/itt_equal.prlb
Properties	metaprl/theories/itt/itt_equal.prlb
+54 -9	metaprl/theories/itt/itt_fun.ml
+380 -3	metaprl/theories/itt/itt_logic.ml
+22 -1	metaprl/theories/itt/itt_logic.mli
+20 -5	metaprl/theories/itt/itt_squash.ml
+3 -0	metaprl/theories/itt/itt_squash.mli
+21 -3	metaprl/theories/itt/itt_struct.ml
+3 -0	metaprl/theories/itt/itt_struct.mli
+8 -3	metaprl/theories/itt/itt_subtype.ml
+1 -0	metaprl/theories/itt/itt_theory.ml
+1 -0	metaprl/theories/itt/itt_theory.mli
+0 -1	metaprl/theories/itt/itt_unit.ml
+5 -2	metaprl/theories/itt/itt_void.ml
+1 -1	metaprl/theories/itt/itt_void.mli
+1 -0	metaprl/theories/lf/Makefile
+1 -0	metaprl/theories/ocaml/Makefile
+1 -0	metaprl/theories/ocaml_sos/Makefile
+1 -0	metaprl/theories/tactic/Makefile
+1 -0	metaprl/theories/tactic/sequent.ml
+1 -0	metaprl/theories/tactic/sequent.mli
+14 -0	metaprl/theories/tactic/tactic_type.ml
+2 -0	metaprl/theories/tactic/tactic_type.mli
+1 -1	metaprl/theories/tactic/tacticals.ml