Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-11 11:14:25 -0800 (Fri, 11 Dec 1998)
Revision: 2522
Log message:

      Fixed some "this expression should have type unit" Ocaml-2.01 warnings
      

Changes  Path
+1 -1 metaprl/library/basic.ml
+11 -10 metaprl/library/db.ml
+1 -1 metaprl/library/library.ml
+14 -13 metaprl/library/library_type_base.ml
+4 -4 metaprl/library/mathBus.ml
+6 -6 metaprl/library/mbterm.ml
+3 -2 metaprl/library/oidtable.ml
+32 -28 metaprl/library/orb.ml
+1 -1 metaprl/mllib/debug_string_sets.ml
+5 -5 metaprl/mllib/hash_set.ml
+6 -5 metaprl/mllib/red_black_set.ml
+2 -2 metaprl/mllib/remote_queue_null.ml
+1 -1 metaprl/mllib/simplehash_sig.ml
+1 -2 metaprl/mllib/simplehashtbl.ml
+10 -10 metaprl/refiner/refiner/refine.mlp
+4 -4 metaprl/refiner/reflib/rformat.ml
+1 -1 metaprl/refiner/reflib/term_dtable.ml
+1 -1 metaprl/refiner/reflib/term_table.ml
+7 -7 metaprl/refiner/term_ds/term_base_ds.mlp
+1 -1 metaprl/refiner/term_ds/term_subst_ds.mlp
+1 -1 metaprl/refiner/term_std/term_subst_std.mlp

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-12-17 07:57:52 -0800 (Thu, 17 Dec 1998)
Revision: 2523
Log message:

      added improvements to mathbus speed, and functionality for edits in nuprl
      

Changes  Path
+39 -11 metaprl/editor/ml/library_eval.ml
+1 -0 metaprl/editor/ml/library_eval.mli
+2 -0 metaprl/editor/ml/library_test.mli
+1 -0 metaprl/library/basic.ml
+1 -0 metaprl/library/basic.mli
+43 -5 metaprl/library/db.ml
+1 -0 metaprl/library/link.ml
+56 -26 metaprl/library/mathBus.ml
+5 -8 metaprl/library/mathBus.mli
+9 -2 metaprl/library/mbterm.ml
+1 -0 metaprl/library/mbterm.mli
+16 -0 metaprl/library/registry.ml
+4 -0 metaprl/library/registry.mli
+4 -0 metaprl/library/registry.txt
Added metaprl/mbs-mpl.txt
Properties metaprl/mbs-mpl.txt

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-22 21:11:43 -0800 (Tue, 22 Dec 1998)
Revision: 2524
Log message:

      Copied the DAG-based unification algorithm
      from the Term_ds module, so that we can run
      FOL performance tests using both Term modules.
      
      When [if] we write a better unification algorithm,
      we should remember to change it in both Term modules
      

Changes  Path
+127 -99 metaprl/refiner/term_std/term_subst_std.mlp

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-28 13:07:52 -0800 (Mon, 28 Dec 1998)
Revision: 2525
Log message:

      Numerous minor changes.
      
      Added itt_fset: a theory of finite sets based on a list
      implementation quotiented by equivalence under arbitrary
      occurrences and ordering.
      
      Added initial reflection theory.  Terms are quotiented by
      alpha-equality, so normal well-formedness proofs are difficult,
      and more work needs to be done to define free variables and
      substitution.
      

Changes  Path
Added metaprl/editor/ml/mp_fol_type2.txt
Properties metaprl/editor/ml/mp_fol_type2.txt
+1 -1 metaprl/editor/ml/mptop
+18 -6 metaprl/editor/ml/package_info.ml
+1 -1 metaprl/editor/ml/shell.ml
+3 -1 metaprl/editor/ml/shell_mp.ml
+27 -23 metaprl/editor/ml/shell_rewrite.ml
+1 -1 metaprl/editor/ml/shell_rule.ml
Added metaprl/editor/ml/tutorial.ml
Properties metaprl/editor/ml/tutorial.ml
Added metaprl/editor/ml/tutorial_itt.ml
Properties metaprl/editor/ml/tutorial_itt.ml
+6 -8 metaprl/editor/ml/w.ml
+1 -0 metaprl/editor/ml/x.ml
+8 -4 metaprl/editor/ml/y.ml
Added metaprl/lib/mbs-mpl.txt
Properties metaprl/lib/mbs-mpl.txt
Deleted metaprl/mbs-mpl.txt
+6 -5 metaprl/mllib/splay_table.mli
+11 -22 metaprl/refiner/refiner/refine.mlp
+4 -4 metaprl/refiner/refsig/refine_sig.ml
+5 -4 metaprl/refiner/refsig/term_addr_sig.ml
+10 -4 metaprl/refiner/refsig/term_op_sig.ml
+55 -5 metaprl/refiner/term_ds/term_addr_ds.mlp
+63 -6 metaprl/refiner/term_ds/term_op_ds.mlp
+13 -13 metaprl/refiner/term_ds/term_subst_ds.mlp
+2 -0 metaprl/refiner/term_gen/term_addr_gen.mlp
+48 -4 metaprl/refiner/term_std/term_op_std.mlp
+9 -4 metaprl/theories/base/base_dtactic.ml
+5 -4 metaprl/theories/base/base_dtactic.mli
+5 -5 metaprl/theories/base/base_rewrite.mli
+5 -4 metaprl/theories/base/base_theory.mlz
+123 -18 metaprl/theories/base/typeinf.ml
+15 -5 metaprl/theories/base/typeinf.mli
+2 -3 metaprl/theories/fol/Makefile
+6 -3 metaprl/theories/fol/fol_all.ml
Added metaprl/theories/fol/fol_all_itt.ml
Properties metaprl/theories/fol/fol_all_itt.ml
Added metaprl/theories/fol/fol_all_itt.mli
Properties metaprl/theories/fol/fol_all_itt.mli
Binary metaprl/theories/fol/fol_all_itt.prlb
Properties metaprl/theories/fol/fol_all_itt.prlb
Added metaprl/theories/fol/fol_bisect_itt.ml
Properties metaprl/theories/fol/fol_bisect_itt.ml
Added metaprl/theories/fol/fol_bisect_itt.mli
Properties metaprl/theories/fol/fol_bisect_itt.mli
Binary metaprl/theories/fol/fol_ctheory.prlb
Properties metaprl/theories/fol/fol_ctheory.prlb
+2 -2 metaprl/theories/fol/fol_exists.ml
+1 -1 metaprl/theories/fol/fol_implies.ml
Binary metaprl/theories/fol/fol_not.prlb
Added metaprl/theories/fol/fol_theory.ml
Properties metaprl/theories/fol/fol_theory.ml
Added metaprl/theories/fol/fol_theory.mli
Properties metaprl/theories/fol/fol_theory.mli
Binary metaprl/theories/fol/fol_theory.prlb
Properties metaprl/theories/fol/fol_theory.prlb
+35 -0 metaprl/theories/fol/fol_type.ml
+4 -0 metaprl/theories/fol/fol_type.mli
Added metaprl/theories/fol/fol_type_itt.ml
Properties metaprl/theories/fol/fol_type_itt.ml
Added metaprl/theories/fol/fol_type_itt.mli
Properties metaprl/theories/fol/fol_type_itt.mli
Binary metaprl/theories/fol/fol_type_itt.prlb
Properties metaprl/theories/fol/fol_type_itt.prlb
+4 -1 metaprl/theories/fol/fol_univ.ml
+1 -0 metaprl/theories/fol/fol_univ.mli
Added metaprl/theories/fol/fol_univ_itt.ml
Properties metaprl/theories/fol/fol_univ_itt.ml
Added metaprl/theories/fol/fol_univ_itt.mli
Properties metaprl/theories/fol/fol_univ_itt.mli
Binary metaprl/theories/fol/fol_univ_itt.prlb
Properties metaprl/theories/fol/fol_univ_itt.prlb
+6 -0 metaprl/theories/itt/Makefile
+21 -4 metaprl/theories/itt/itt_atom.ml
+5 -7 metaprl/theories/itt/itt_atom.mli
Added metaprl/theories/itt/itt_atom_bool.ml
Properties metaprl/theories/itt/itt_atom_bool.ml
Added metaprl/theories/itt/itt_atom_bool.mli
Properties metaprl/theories/itt/itt_atom_bool.mli
Added metaprl/theories/itt/itt_bisect.ml
Properties metaprl/theories/itt/itt_bisect.ml
Added metaprl/theories/itt/itt_bisect.mli
Properties metaprl/theories/itt/itt_bisect.mli
Binary metaprl/theories/itt/itt_bisect.prlb
Properties metaprl/theories/itt/itt_bisect.prlb
+607 -34 metaprl/theories/itt/itt_bool.ml
+45 -7 metaprl/theories/itt/itt_bool.mli
Binary metaprl/theories/itt/itt_bool.prlb
Properties metaprl/theories/itt/itt_bool.prlb
Added metaprl/theories/itt/itt_bunion.ml
Properties metaprl/theories/itt/itt_bunion.ml
Added metaprl/theories/itt/itt_bunion.mli
Properties metaprl/theories/itt/itt_bunion.mli
Binary metaprl/theories/itt/itt_bunion.prlb
Properties metaprl/theories/itt/itt_bunion.prlb
+13 -4 metaprl/theories/itt/itt_dprod.ml
+100 -5 metaprl/theories/itt/itt_equal.ml
+25 -4 metaprl/theories/itt/itt_equal.mli
Binary metaprl/theories/itt/itt_equal.prlb
Added metaprl/theories/itt/itt_fset.ml
Properties metaprl/theories/itt/itt_fset.ml
Added metaprl/theories/itt/itt_fset.mli
Properties metaprl/theories/itt/itt_fset.mli
Binary metaprl/theories/itt/itt_fset.prlb
Properties metaprl/theories/itt/itt_fset.prlb
+12 -0 metaprl/theories/itt/itt_int.ml
+1 -3 metaprl/theories/itt/itt_int.mli
+53 -12 metaprl/theories/itt/itt_int_bool.ml
+71 -7 metaprl/theories/itt/itt_isect.ml
+10 -5 metaprl/theories/itt/itt_isect.mli
Binary metaprl/theories/itt/itt_isect.prlb
Properties metaprl/theories/itt/itt_isect.prlb
+96 -3 metaprl/theories/itt/itt_list.ml
+6 -0 metaprl/theories/itt/itt_list.mli
Binary metaprl/theories/itt/itt_list.prlb
Properties metaprl/theories/itt/itt_list.prlb
Added metaprl/theories/itt/itt_list2.ml
Properties metaprl/theories/itt/itt_list2.ml
Added metaprl/theories/itt/itt_list2.mli
Properties metaprl/theories/itt/itt_list2.mli
Binary metaprl/theories/itt/itt_list2.prlb
Properties metaprl/theories/itt/itt_list2.prlb
+19 -9 metaprl/theories/itt/itt_logic.ml
+5 -4 metaprl/theories/itt/itt_logic.mli
+57 -24 metaprl/theories/itt/itt_quotient.ml
+13 -11 metaprl/theories/itt/itt_quotient.mli
+8 -5 metaprl/theories/itt/itt_rfun.ml
+60 -94 metaprl/theories/itt/itt_set.ml
+6 -24 metaprl/theories/itt/itt_set.mli
+57 -9 metaprl/theories/itt/itt_srec.ml
+5 -5 metaprl/theories/itt/itt_srec.mli
+1 -4 metaprl/theories/itt/itt_struct.ml
+74 -18 metaprl/theories/itt/itt_subtype.ml
+23 -10 metaprl/theories/itt/itt_subtype.mli
+18 -1 metaprl/theories/itt/itt_theory.ml
+11 -5 metaprl/theories/itt/itt_theory.mli
Added metaprl/theories/itt/itt_tsub.ml
Properties metaprl/theories/itt/itt_tsub.ml
Added metaprl/theories/itt/itt_tsub.mli
Properties metaprl/theories/itt/itt_tsub.mli
Added metaprl/theories/itt/itt_tunion.ml
Properties metaprl/theories/itt/itt_tunion.ml
Added metaprl/theories/itt/itt_tunion.mli
Properties metaprl/theories/itt/itt_tunion.mli
+33 -4 metaprl/theories/itt/itt_union.ml
+22 -4 metaprl/theories/itt/itt_unit.ml
+10 -4 metaprl/theories/itt/itt_unit.mli
+6 -6 metaprl/theories/itt/itt_void.ml
+5 -4 metaprl/theories/itt/itt_void.mli
+5 -1 metaprl/theories/reflect_itt/Makefile
Added metaprl/theories/reflect_itt/refl_free_vars.ml
Properties metaprl/theories/reflect_itt/refl_free_vars.ml
Added metaprl/theories/reflect_itt/refl_free_vars.mli
Properties metaprl/theories/reflect_itt/refl_free_vars.mli
Binary metaprl/theories/reflect_itt/refl_free_vars.prlb
Properties metaprl/theories/reflect_itt/refl_free_vars.prlb
Added metaprl/theories/reflect_itt/refl_raw_term.ml
Properties metaprl/theories/reflect_itt/refl_raw_term.ml
Added metaprl/theories/reflect_itt/refl_raw_term.mli
Properties metaprl/theories/reflect_itt/refl_raw_term.mli
Binary metaprl/theories/reflect_itt/refl_raw_term.prlb
Properties metaprl/theories/reflect_itt/refl_raw_term.prlb
+696 -183 metaprl/theories/reflect_itt/refl_term.ml
+96 -77 metaprl/theories/reflect_itt/refl_term.mli
Binary metaprl/theories/reflect_itt/refl_term.prlb
Added metaprl/theories/reflect_itt/refl_var.ml
Properties metaprl/theories/reflect_itt/refl_var.ml
Added metaprl/theories/reflect_itt/refl_var.mli
Properties metaprl/theories/reflect_itt/refl_var.mli
Binary metaprl/theories/reflect_itt/refl_var.prlb
Properties metaprl/theories/reflect_itt/refl_var.prlb
Added metaprl/theories/reflect_itt/refl_var_set.ml
Properties metaprl/theories/reflect_itt/refl_var_set.ml
Added metaprl/theories/reflect_itt/refl_var_set.mli
Properties metaprl/theories/reflect_itt/refl_var_set.mli
Binary metaprl/theories/reflect_itt/refl_var_set.prlb
Properties metaprl/theories/reflect_itt/refl_var_set.prlb
+114 -4 metaprl/theories/tactic/conversionals.ml
+19 -4 metaprl/theories/tactic/conversionals.mli
+19 -9 metaprl/theories/tactic/mptop.ml
+70 -126 metaprl/theories/tactic/rewrite_type.ml
+7 -21 metaprl/theories/tactic/rewrite_type.mli
+12 -4 metaprl/theories/tactic/sequent.ml
+9 -4 metaprl/theories/tactic/sequent.mli
+61 -6 metaprl/theories/tactic/tactic_type.ml
+24 -5 metaprl/theories/tactic/tactic_type.mli
+9 -4 metaprl/theories/tactic/tacticals.ml
+6 -4 metaprl/theories/tactic/tacticals.mli
+72 -4 metaprl/theories/tactic/var.ml
+8 -4 metaprl/theories/tactic/var.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-28 17:36:10 -0800 (Mon, 28 Dec 1998)
Revision: 2526
Log message:

      Cleenup
      

Changes  Path
+1 -1 metaprl/mk/config
+1 -1 metaprl/mllib/Makefile
+1 -0 metaprl/refiner/reflib/Makefile
Deleted metaprl/theories/fol/fol_theory.mlz
+2 -0 metaprl/theories/tptp/Makefile
+1 -1 metaprl/util/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-29 11:11:40 -0800 (Tue, 29 Dec 1998)
Revision: 2527
Log message:

      Proof expansion works.
      Fixed a bad typo in red_black_set.
      

Changes  Path
+28 -5 metaprl/editor/ml/io_proof.ml
+8 -4 metaprl/editor/ml/io_proof.mli
+16 -13 metaprl/editor/ml/package_df.ml
+24 -6 metaprl/editor/ml/package_info.ml
+6 -5 metaprl/editor/ml/package_type.mlz
+41 -34 metaprl/editor/ml/proof.ml
+12 -5 metaprl/editor/ml/proof.mli
+6 -0 metaprl/editor/ml/proof_edit.ml
+1 -0 metaprl/editor/ml/proof_edit.mli
+8 -6 metaprl/editor/ml/proof_step.ml
+5 -4 metaprl/editor/ml/proof_step.mli
+16 -4 metaprl/editor/ml/shell.ml
+4 -0 metaprl/editor/ml/shell_mp.ml
+2 -2 metaprl/editor/ml/w.ml
+3 -2 metaprl/editor/ml/y.ml
+18 -10 metaprl/mllib/red_black_set.ml
+2 -1 metaprl/theories/tactic/rewrite_type.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-29 12:14:09 -0800 (Tue, 29 Dec 1998)
Revision: 2528
Log message:

      Added "kreitz" command to fold up an entire proof subtree into a single node.
      

Changes  Path
+69 -0 metaprl/editor/ml/proof.ml
+6 -0 metaprl/editor/ml/proof.mli
+1 -0 metaprl/editor/ml/proof_edit.ml
+1 -0 metaprl/editor/ml/proof_edit.mli
+9 -1 metaprl/editor/ml/shell.ml
+1 -0 metaprl/editor/ml/shell.mli
+2 -1 metaprl/editor/ml/shell_null.ml
+5 -1 metaprl/editor/ml/shell_rewrite.ml
+5 -1 metaprl/editor/ml/shell_rule.ml
+2 -1 metaprl/editor/ml/shell_type.mlz
+6 -5 metaprl/refiner/reflib/dform.ml
Binary metaprl/theories/reflect_itt/refl_term.prlb

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-29 15:30:21 -0800 (Tue, 29 Dec 1998)
Revision: 2529
Log message:

      Added pigeonhole problem in editor/ml/test.ml.
      
      To try it:
      
      % ./mptop
      # #use "y.ml";;
      # refine timingT proveT;;
      

Changes  Path
+1 -0 metaprl/editor/ml/Makefile
+112 -20 metaprl/editor/ml/test.ml
+1 -1 metaprl/editor/ml/test.mli
+3 -29 metaprl/editor/ml/y.ml
+8 -8 metaprl/filter/term_grammar.ml
+5 -3 metaprl/theories/itt/itt_logic.ml
+1 -0 metaprl/theories/itt/itt_logic.mli
+31 -34 metaprl/theories/itt/itt_prop_decide.ml
+5 -5 metaprl/theories/itt/itt_prop_decide.mli
+1 -1 metaprl/theories/itt/itt_theory.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-29 19:03:47 -0800 (Tue, 29 Dec 1998)
Revision: 2530
Log message:

      Added pigeonhole generator.
      

Changes  Path
Added metaprl/editor/ml/pigeon.ml
Properties metaprl/editor/ml/pigeon.ml
+743 -22 metaprl/editor/ml/test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-29 19:58:59 -0800 (Tue, 29 Dec 1998)
Revision: 2531
Log message:

      The general intuitionistic propDecideT now works.
      There was a bug in Itt_logic preventing << false >> from
      being recognized.
      

Changes  Path
+157 -0 metaprl/editor/ml/test.ml
+1 -0 metaprl/editor/ml/test.mli
+4 -2 metaprl/theories/itt/itt_logic.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-30 10:53:59 -0800 (Wed, 30 Dec 1998)
Revision: 2532
Log message:

      Made bound_term'=bound_term.
      This does not save much time, but it saves some memory (10% on PHP example)
      

Changes  Path
+5 -8 metaprl/refiner/term_ds/term_addr_ds.mlp
+23 -66 metaprl/refiner/term_ds/term_base_ds.mlp
+1 -4 metaprl/refiner/term_ds/term_ds.ml
+1 -4 metaprl/refiner/term_ds/term_ds_sig.ml
+9 -15 metaprl/refiner/term_ds/term_eval_ds.mlp
+6 -18 metaprl/refiner/term_ds/term_man_ds.mlp
+94 -228 metaprl/refiner/term_ds/term_op_ds.mlp
+15 -28 metaprl/refiner/term_ds/term_subst_ds.mlp

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-30 16:41:51 -0800 (Wed, 30 Dec 1998)
Revision: 2533
Log message:

      Small efficiency fixes.
      Makes Pigeon4-ProveT 5% faster.
      

Changes  Path
+10 -11 metaprl/refiner/rewrite/rewrite_match_redex.mlp

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-30 17:56:48 -0800 (Wed, 30 Dec 1998)
Revision: 2534
Log message:

      Pushed Sequent.hyp_indices down into the Term_man
      This gives 2% speedup on Pigeon4-ProveT.
      

Changes  Path
+1 -0 metaprl/refiner/refsig/term_man_sig.ml
+17 -10 metaprl/refiner/term_ds/term_man_ds.mlp
+25 -19 metaprl/refiner/term_gen/term_man_gen.mlp
+1 -9 metaprl/theories/tactic/sequent.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-30 18:02:48 -0800 (Wed, 30 Dec 1998)
Revision: 2535
Log message:

      Fixed the bytecode profiling build.
      
      Since ocamlcp does not allow threads,
      the profiled bytecode is compiled without the -thread option
      

Changes  Path
+5 -1 metaprl/Makefile
+7 -2 metaprl/mk/config
+0 -1 metaprl/mk/preface

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-30 18:40:22 -0800 (Wed, 30 Dec 1998)
Revision: 2536
Log message:

      Inlined extract_sequent_terms.
      
      This gives another 2% on Pigeon4-ProveT
      

Changes  Path
+6 -12 metaprl/refiner/rewrite/rewrite_match_redex.mlp

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-30 18:48:31 -0800 (Wed, 30 Dec 1998)
Revision: 2537
Log message:

      Do not call get_core unless the sequent is actually a delayed substitution.
      
      Another 1% on PHP4 example
      

Changes  Path
+17 -11 metaprl/refiner/term_ds/term_man_ds.mlp

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-31 09:23:10 -0800 (Thu, 31 Dec 1998)
Revision: 2538
Log message:

      Added module-checking function "expand_all" to the Shell module.
      

Changes  Path
+6 -6 metaprl/editor/ml/proof_edit.ml
+94 -21 metaprl/editor/ml/shell.ml
+2 -0 metaprl/editor/ml/shell.mli
+1 -1 metaprl/editor/ml/w.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-31 14:31:08 -0800 (Thu, 31 Dec 1998)
Revision: 2539
Log message:

      The list of include directories is now defined in mpconfig
      to avoid redundancy and to ensure that mp, mptop and mpopt
      use the same list (mpopt was missing some directories).
      

Changes  Path
+1 -1 metaprl/editor/ml/mp
+1 -0 metaprl/editor/ml/mpconfig
+1 -1 metaprl/editor/ml/mpopt
+1 -1 metaprl/editor/ml/mptop

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-31 15:09:29 -0800 (Thu, 31 Dec 1998)
Revision: 2540
Log message:

      debug_unify
      

Changes  Path
+3 -1 metaprl/refiner/term_ds/term_subst_ds.mlp
+16 -2 metaprl/refiner/term_std/term_subst_std.mlp

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-31 15:38:40 -0800 (Thu, 31 Dec 1998)
Revision: 2541
Log message:

      debug_alpha_equal
      

Changes  Path
+29 -2 metaprl/refiner/term_ds/term_subst_ds.mlp
+23 -11 metaprl/refiner/term_std/term_subst_std.mlp

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-31 15:39:42 -0800 (Thu, 31 Dec 1998)
Revision: 2542
Log message:

      Faster propDecideT.
      

Changes  Path
+83 -31 metaprl/editor/ml/test.ml
+1 -1 metaprl/editor/ml/y.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-31 15:54:50 -0800 (Thu, 31 Dec 1998)
Revision: 2543
Log message:

      Print terms in debug_alpha_equal
      

Changes  Path
+1 -2 metaprl/refiner/term_ds/term_subst_ds.mlp
+2 -2 metaprl/refiner/term_std/term_subst_std.mlp

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-12-31 16:17:40 -0800 (Thu, 31 Dec 1998)
Revision: 2544
Log message:

      Fixed debug
      

Changes  Path
+3 -3 metaprl/refiner/term_std/term_subst_std.mlp