Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-01 06:57:13 -0700 (Mon, 01 Jun 1998)
Revision: 2209
Log message:

      Proving twice one is two.
      

Changes	Path
+4 -5	metaprl/editor/ml/Makefile
+4 -2	metaprl/editor/ml/io_proof.ml
+3 -1	metaprl/editor/ml/io_proof_type.mlz
+1 -0	metaprl/editor/ml/make1
+6 -3	metaprl/editor/ml/nl
+3 -25	metaprl/editor/ml/package_info.ml
+3 -1	metaprl/editor/ml/package_info.mli
+4 -2	metaprl/editor/ml/package_int.ml
+3 -10	metaprl/editor/ml/package_type.mlz
+3 -4	metaprl/editor/ml/proof.ml
+3 -1	metaprl/editor/ml/proof_edit.ml
+4 -1	metaprl/editor/ml/proof_step.ml
+3 -1	metaprl/editor/ml/proof_step.mli
+72 -53	metaprl/editor/ml/shell.ml
+4 -2	metaprl/editor/ml/shell.mli
+140 -15	metaprl/editor/ml/shell_p4.ml
+7 -0	metaprl/editor/ml/shell_p4.mli
+18 -4	metaprl/editor/ml/shell_rewrite.ml
+3 -1	metaprl/editor/ml/shell_type.mlz
+7 -9	metaprl/editor/ml/test.ml
+6 -2	metaprl/editor/ml/test.mli
+55 -48	metaprl/filter/Makefile
+3 -2	metaprl/filter/buffer.ml
+3 -3	metaprl/filter/filter_bin.ml
+3 -8	metaprl/filter/filter_cache.ml
+3 -2	metaprl/filter/filter_cache.mli
+6 -19	metaprl/filter/filter_cache_fun.ml
+3 -1	metaprl/filter/filter_cache_fun.mli
+4 -6	metaprl/filter/filter_comment.ml
+4 -0	metaprl/filter/filter_exn.ml
+4 -2	metaprl/filter/filter_hash.ml
+4 -2	metaprl/filter/filter_html.ml
+3 -10	metaprl/filter/filter_ocaml.ml
+5 -65	metaprl/filter/filter_parse.ml
+17 -64	metaprl/filter/filter_prog.ml
+3 -1	metaprl/filter/filter_prog.mli
+5 -17	metaprl/filter/filter_summary.ml
+3 -20	metaprl/filter/filter_summary_io.ml
+3 -7	metaprl/filter/filter_summary_type.mlz
+4 -1	metaprl/filter/filter_type.mlz
+3 -2	metaprl/filter/infix.pre.ml
+3 -8	metaprl/filter/mLast_util.ml
+36 -14	metaprl/filter/prlcomp.ml
+4 -114	metaprl/filter/term_grammar.ml
+3 -1	metaprl/filter/term_quote.ml
+3 -24	metaprl/filter/test_gram.ml
+6 -20	metaprl/horus/term.ml
+3 -2	metaprl/horus/term.mli
+16 -19	metaprl/library/ascii_scan.ml
+3 -3	metaprl/library/ascii_scan.mli
+41 -43	metaprl/library/basic.ml
+1 -3	metaprl/library/basic.mli
+2 -3	metaprl/library/bigInt.ml
+78 -96	metaprl/library/db.ml
+51 -58	metaprl/library/definition.ml
+4 -4	metaprl/library/definition.mli
+2 -3	metaprl/library/int32.ml
+1 -1	metaprl/library/int32.mli
+47 -52	metaprl/library/library.ml
+18 -19	metaprl/library/library.mli
+4 -6	metaprl/library/library_eval.ml
+1 -1	metaprl/library/library_eval.mli
+5 -9	metaprl/library/link.ml
+1 -1	metaprl/library/link.mli
+52 -85	metaprl/library/mathBus.ml
+2 -3	metaprl/library/mathBus.mli
+24 -27	metaprl/library/mbterm.ml
+1 -1	metaprl/library/mbterm.mli
+0 -1	metaprl/library/nuprl5.ml
+1 -1	metaprl/library/object_id.ml
+1 -1	metaprl/library/object_id.mli
+2 -2	metaprl/library/oidtable.ml
+0 -1	metaprl/library/oidtable.mli
+76 -90	metaprl/library/orb.ml
+1 -2	metaprl/library/orb.mli
+8 -12	metaprl/library/registry.ml
+2 -3	metaprl/library/registry.mli
+7 -7	metaprl/library/socketIo.ml
+0 -1	metaprl/library/socketIo.mli
+15 -22	metaprl/library/tentfunctor.ml
+43 -49	metaprl/library/test.ml
+0 -1	metaprl/library/test.mli
+11 -15	metaprl/library/utils.ml
+2 -2	metaprl/library/utils.mli
+54 -48	metaprl/mk/config
+3 -1	metaprl/mllib/ctype.mli
+3 -4	metaprl/mllib/dag.mlz
+4 -1	metaprl/mllib/debug_set.ml
+6 -5	metaprl/mllib/env_arg.ml
+3 -20	metaprl/mllib/file_base.ml
+3 -7	metaprl/mllib/file_base_type.ml
+3 -4	metaprl/mllib/file_type_base.ml
+3 -27	metaprl/mllib/imp_dag.ml
+15 -12	metaprl/mllib/list_util.ml
+4 -1	metaprl/mllib/string_util.ml
+3 -1	metaprl/refiner/refbase/opname.ml
+30 -8	metaprl/refiner/refiner/rewrite.ml
+23 -8	metaprl/refiner/reflib/dform.ml
+3 -1	metaprl/refiner/reflib/dform.mli
+3 -1	metaprl/refiner/reflib/dform_print.ml
+3 -5	metaprl/refiner/reflib/ml_file.ml
+3 -45	metaprl/refiner/reflib/ml_format.ml
+3 -7	metaprl/refiner/reflib/ml_print.ml
+3 -5	metaprl/refiner/reflib/ml_print_sig.mlz
+3 -2	metaprl/refiner/reflib/ml_string.ml
+4 -5	metaprl/refiner/reflib/rformat.ml
+4 -5	metaprl/refiner/reflib/term_dtable.ml
+4 -3	metaprl/refiner/reflib/term_stable.ml
+3 -1	metaprl/refiner/reflib/term_table.ml
+4 -1	metaprl/refiner/reflib/term_template.ml
+3 -12	metaprl/refiner/refsig/rewrite_sig.ml
+3 -1	metaprl/refiner/refsig/term_addr_sig.ml
+3 -13	metaprl/refiner/refsig/term_man_sig.ml
+3 -1	metaprl/refiner/refsig/term_meta_sig.ml
+3 -20	metaprl/refiner/refsig/term_op_sig.ml
+3 -3	metaprl/refiner/refsig/term_sig.ml
+3 -3	metaprl/refiner/refsig/term_subst_sig.ml
+29 -29	metaprl/refiner/term_ds/term_ds.ml
+5 -5	metaprl/refiner/term_ds/term_ds.mli
+44 -44	metaprl/refiner/term_ds/term_op_ds.ml
+5 -2	metaprl/refiner/term_gen/term_meta_gen.ml
+5 -2	metaprl/refiner/term_gen/term_meta_gen.mli
+8 -2	metaprl/refiner/term_std/term_addr_std.ml
+16 -4	metaprl/refiner/term_std/term_man_std.ml
+6 -3	metaprl/refiner/term_std/term_std.ml
+3 -2	metaprl/theories/base/base_cache.ml
+15 -3	metaprl/theories/base/base_dform.ml
+21 -17	metaprl/theories/base/base_dform.mli
+4 -5	metaprl/theories/base/base_dtactic.ml
+28 -30	metaprl/theories/base/evaluator.ml
+3 -3	metaprl/theories/base/typeinf.ml
+3 -1	metaprl/theories/base/typeinf.mli
+4 -1	metaprl/theories/czf/czf_struct.mli
+10 -6	metaprl/theories/itt/itt_atom.ml
+6 -1	metaprl/theories/itt/itt_dfun.ml
+14 -8	metaprl/theories/itt/itt_dprod.ml
+18 -14	metaprl/theories/itt/itt_equal.ml
+3 -2	metaprl/theories/itt/itt_equal.mli
+6 -1	metaprl/theories/itt/itt_fun.ml
+23 -21	metaprl/theories/itt/itt_int.ml
+9 -3	metaprl/theories/itt/itt_isect.ml
+10 -7	metaprl/theories/itt/itt_list.ml
+3 -1	metaprl/theories/itt/itt_list.mli
+21 -28	metaprl/theories/itt/itt_logic.ml
+4 -1	metaprl/theories/itt/itt_prec.ml
+4 -1	metaprl/theories/itt/itt_prec.mli
+9 -3	metaprl/theories/itt/itt_prod.ml
+4 -1	metaprl/theories/itt/itt_prod.mli
+10 -5	metaprl/theories/itt/itt_quotient.ml
+4 -1	metaprl/theories/itt/itt_quotient.mli
+14 -14	metaprl/theories/itt/itt_redrules.ml
+15 -9	metaprl/theories/itt/itt_rfun.ml
+12 -9	metaprl/theories/itt/itt_set.ml
+7 -3	metaprl/theories/itt/itt_soft.ml
+5 -2	metaprl/theories/itt/itt_soft.mli
+4 -4	metaprl/theories/itt/itt_squash.ml
+3 -1	metaprl/theories/itt/itt_squash.mli
+9 -5	metaprl/theories/itt/itt_srec.ml
+9 -6	metaprl/theories/itt/itt_srec.mli
+9 -2	metaprl/theories/itt/itt_struct.ml
+8 -6	metaprl/theories/itt/itt_subtype.ml
+3 -1	metaprl/theories/itt/itt_subtype.mli
+8 -1	metaprl/theories/itt/itt_union.ml
+4 -1	metaprl/theories/itt/itt_union.mli
+5 -1	metaprl/theories/itt/itt_unit.ml
+5 -1	metaprl/theories/itt/itt_void.ml
+3 -1	metaprl/theories/lf/lf_ctx.mli
+3 -2	metaprl/theories/lf/lf_sig.mli
+3 -8	metaprl/theories/ocaml/ocaml.mlz
+2 -2	metaprl/theories/ocaml/ocaml_df.ml
+2 -2	metaprl/theories/ocaml/ocaml_df.mli
+3 -1	metaprl/theories/ocaml/ocaml_expr_df.ml
+3 -2	metaprl/theories/ocaml/ocaml_patt_df.ml
+4 -1	metaprl/theories/ocaml/ocaml_str_df.ml
+3 -1	metaprl/theories/ocaml/ocaml_type_df.ml
+4 -1	metaprl/theories/ocaml_sos/ocaml_base_sos.ml
+4 -1	metaprl/theories/ocaml_sos/ocaml_base_sos.mli
+7 -13	metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+8 -14	metaprl/theories/ocaml_sos/ocaml_expr_sos.mli
+3 -4	metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+3 -4	metaprl/theories/ocaml_sos/ocaml_patt_sos.mli
+3 -3	metaprl/theories/rewrite/rw_beta.ml
+6 -33	metaprl/theories/tactic/tactic_cache.ml
+3 -1	metaprl/theories/tactic/tactic_cache.mli
+5 -2	metaprl/theories/tactic/tactic_type.mlz
+4 -4	metaprl/theories/tactic/tacticals.ml
Properties	metaprl/util
+4 -2	metaprl/util/Makefile
+1 -1	metaprl/util/misc.mli