Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-02 01:00:18 -0800 (Mon, 02 Dec 2002)
Revision: 3942
Log message:

      Added expand_all to mp.run top-lop
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-12-03 05:16:48 -0800 (Tue, 03 Dec 2002)
Revision: 3943
Log message:

      Meta conversions are eliminated from code.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-12-08 19:41:12 -0800 (Sun, 08 Dec 2002)
Revision: 3946
Log message:

      arithT is ready at first glance.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-12-09 19:13:44 -0800 (Mon, 09 Dec 2002)
Revision: 3947
Log message:

      Some code clean up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-09 20:56:12 -0800 (Mon, 09 Dec 2002)
Revision: 3948
Log message:

      - For some reason hash table resize used the folrmula
      x := ((x+1)*2)-1
      instead of just
      x := (x*2) + 1
      ...
      
      - Added a version of mpxterm script that uses a slightly larger font
      (useful for demos).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-09 21:52:03 -0800 (Mon, 09 Dec 2002)
Revision: 3949
Log message:

      - Added proper intro_typeinf annotations on a number of _wf theorems.
      - Modified an incomplete proof of itt_list2/nth_wf to demonstrate new
      arith-related issues.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-10 01:51:34 -0800 (Tue, 10 Dec 2002)
Revision: 3950
Log message:

      Proved rev_wf
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-12-10 18:17:46 -0800 (Tue, 10 Dec 2002)
Revision: 3952
Log message:

      cases, when reduceC actually increases the size of the term, are removed from reduce resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-10 19:31:26 -0800 (Tue, 10 Dec 2002)
Revision: 3953
Log message:

      Fixing the problem found by Yegor:
      - Change package status to "Unmodified" whe the package is first loaded.
      - "export" should do a more complete check of package status before attempting
      to export it (ReadOnly and Incomplete packages should not be ever exported).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-12-17 10:25:13 -0800 (Tue, 17 Dec 2002)
Revision: 3957
Log message:

      Fixing the damage caused be reducing reduce-resource (now some things should be told explicitely)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-12-18 14:01:13 -0800 (Wed, 18 Dec 2002)
Revision: 3962
Log message:

      Some addition reduce-rules. Cancelation of bnot(bnot()) added to itt_bool also
      to cover bnot(<=) --> bnot(bnot(<)).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-19 16:30:41 -0800 (Thu, 19 Dec 2002)
Revision: 3964
Log message:

      Proved a few simple rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-20 00:15:46 -0800 (Fri, 20 Dec 2002)
Revision: 3965
Log message:

      Extended the proof of nth_wf a little to provide examples to Yegor.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-20 17:18:28 -0800 (Fri, 20 Dec 2002)
Revision: 3969
Log message:

      Print out the number of nodes when doing status[_all]. Also, include those
      numbers in the totals counted by the scripts.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-20 17:57:00 -0800 (Fri, 20 Dec 2002)
Revision: 3970
Log message:

      Minor fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-20 18:04:05 -0800 (Fri, 20 Dec 2002)
Revision: 3971
Log message:

      Argh, another minor fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-22 18:48:15 -0800 (Sun, 22 Dec 2002)
Revision: 3972
Log message:

      Fixing bug #26.
      Now the Mp_resource module will rais an Invalid_argument exception if there
      are duplicate bookmarks.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-23 00:10:57 -0800 (Mon, 23 Dec 2002)
Revision: 3973
Log message:

      - We used to generase resource "bookmarks" (checkpoints) for all
      the rules/rewrites. Now only interactive/derived/incomplete rules/rewrites
      would have checkpoints while primitive/ml ones would not
      
      - Fixed a bug with resource management (in case where a theory include
      is followed by a resource improvement as opposed to being followed by a bookmark,
      the included data was not inherited)
      
      - Creating a rule/rewrite "edit" object should not require finding a sentinel
      and bookmark (those are only needed only when we want to edit the actual proof).
      
      P.S. This commit have sped up the "status_all" by about 12%.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-25 17:01:51 -0800 (Wed, 25 Dec 2002)
Revision: 3975
Log message:

      Minor clarification.