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