Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-03 15:06:15 -0700 (Fri, 03 Jul 1998)
Revision: 2291
Log message:

      IO terms are now in term_std format.
      

Changes	Path
+420 -131	metaprl/editor/ml/io_proof.ml
+8 -10	metaprl/editor/ml/io_proof.mli
+21 -19	metaprl/editor/ml/io_proof_type.mlz
+5 -0	metaprl/editor/ml/package_df.ml
+8 -3	metaprl/editor/ml/package_df.mli
+20 -10	metaprl/editor/ml/package_info.ml
+8 -5	metaprl/editor/ml/package_type.mlz
+166 -16	metaprl/editor/ml/proof.ml
+6 -2	metaprl/editor/ml/proof.mli
+4 -1	metaprl/editor/ml/proof_edit.ml
+6 -3	metaprl/editor/ml/proof_edit.mli
+187 -48	metaprl/editor/ml/proof_step.ml
+25 -2	metaprl/editor/ml/proof_step.mli
+4 -1	metaprl/editor/ml/proof_type.mlz
+4 -1	metaprl/editor/ml/shell.mli
+4 -1	metaprl/editor/ml/shell_rewrite.ml
+6 -2	metaprl/editor/ml/shell_rewrite.mli
+4 -1	metaprl/editor/ml/shell_rule.ml
+6 -2	metaprl/editor/ml/shell_rule.mli
+4 -1	metaprl/editor/ml/shell_type.mlz
+16 -40	metaprl/filter/filter_cache.ml
+34 -0	metaprl/filter/filter_summary.ml
+5 -0	metaprl/filter/filter_summary.mli
+27 -14	metaprl/mllib/list_util.ml
+6 -1	metaprl/mllib/list_util.mli
+103 -23	metaprl/mllib/memo.ml
+38 -3	metaprl/mllib/memo.mli
+7 -0	metaprl/refiner/refiner/refine_error.ml
+4 -3	metaprl/refiner/refiner/refiner.ml
+7 -4	metaprl/refiner/refiner/refiner_ds_simp.ml
+7 -4	metaprl/refiner/refiner/refiner_std_simp.ml
+1 -1	metaprl/refiner/reflib/Files
+36 -33	metaprl/refiner/reflib/ml_format.ml
+7 -4	metaprl/refiner/reflib/ml_term.ml
+232 -104	metaprl/refiner/reflib/term_copy.ml
+31 -6	metaprl/refiner/reflib/term_copy.mli
+4 -1	metaprl/refiner/refsig/refine_error.h
+4 -0	metaprl/refiner/refsig/refine_error_sig.ml
+4 -0	metaprl/refiner/refsig/refine_error_sig.mli
+3 -2	metaprl/refiner/term_ds/term_base_ds.mlip
+0 -4	metaprl/refiner/term_ds/term_base_ds.mlp
+3 -2	metaprl/refiner/term_ds/term_eval_ds.mlip
+0 -6	metaprl/refiner/term_ds/term_eval_ds.mlp
+3 -2	metaprl/refiner/term_ds/term_op_ds.mlip
+0 -6	metaprl/refiner/term_ds/term_op_ds.mlp
+3 -2	metaprl/refiner/term_ds/term_subst_ds.mlip
+0 -6	metaprl/refiner/term_ds/term_subst_ds.mlp
+0 -1	metaprl/refiner/term_gen/Files
+3 -2	metaprl/refiner/term_std/term_base_std.mlip
+3 -4	metaprl/refiner/term_std/term_base_std.mlp
+3 -2	metaprl/refiner/term_std/term_eval_std.mlip
+3 -6	metaprl/refiner/term_std/term_eval_std.mlp
+3 -2	metaprl/refiner/term_std/term_op_std.mlip
+3 -6	metaprl/refiner/term_std/term_op_std.mlp
+3 -2	metaprl/refiner/term_std/term_subst_std.mlip
+3 -6	metaprl/refiner/term_std/term_subst_std.mlp
+4 -1	metaprl/theories/tactic/sequent.ml
+6 -3	metaprl/theories/tactic/sequent.mli
+31 -7	metaprl/theories/tactic/tactic_type.ml
+15 -8	metaprl/theories/tactic/tactic_type.mli