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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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