Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-08 19:32:14 -0800 (Thu, 08 Jan 2004)
Revision: 318
Log message:

      When comparing symbols, compare ints first, instead of using Pervasives.compare
      right away. This gives another ~4% speedup on "status_all();;".
      

Changes by: yegor (yegor at unknown.email)
Date: 2004-01-20 22:26:07 -0800 (Tue, 20 Jan 2004)
Revision: 319
Log message:

      1.deletemax added to splay_table (and other tables).
      2.itt_supinf has some progress on SupInf, testT there only prints sequence
      of inequalities and I believe they can be proved routinely.
      Right now it works with normalized integer terms, 'greater or equal' only.
      Ideally it should work with ordered fields.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-27 19:32:38 -0800 (Tue, 27 Jan 2004)
Revision: 320
Log message:

      - Made Lm_list_util.flat_map tail-recursive.
      - When there is a label where is does not belong, raise a meaningful error
        at parsing stage, not an abscure one when already in filter_prog.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 18:29:57 -0800 (Wed, 28 Jan 2004)
Revision: 321
Log message:

      Removed all the unused "open" statements.
      

Changes by: yegor (yegor at unknown.email)
Date: 2004-01-28 22:20:24 -0800 (Wed, 28 Jan 2004)
Revision: 322
Log message:

      Lm_splay_table, etc - list_of added,
      it returns content in ascending order of the key.
      
      Itt_rat - some wf-lemmas and properties of max/min/ge added
      
      Itt_supinf - test and test2 have only "trivial" subgoals now, test4 - not yet.
      

Changes by: yegor (yegor at unknown.email)
Date: 2004-01-29 22:59:04 -0800 (Thu, 29 Jan 2004)
Revision: 323
Log message:

      Lm_splay_table - more efficient implementation of list_of.
      Itt_rat - more lemmas for max/min/ge
      Itt_supinf - moving ahead