Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-03 17:58:12 -0800 (Sat, 03 Jan 2004)
Revision: 5219
Log message:

      - Since OCaml ints are 31-bit on 32-bit platform, constats like 0x89ac12bd and
      0xb023821b are illegal on 32-bit platforms (and recent versions of OCaml will
      actually reject them).
      
      - Adding scripts for "check_all" (similar to the ones we have for status_all).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-03 19:39:21 -0800 (Sat, 03 Jan 2004)
Revision: 5220
Log message:

      When using omake, explicitly call for editor/ml/mp.opt
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-04 11:30:48 -0800 (Sun, 04 Jan 2004)
Revision: 5221
Log message:

      Fixing couple of unescaped backslashes.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-05 16:31:38 -0800 (Mon, 05 Jan 2004)
Revision: 5222
Log message:

      Changed according axioms to be primitive.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-05 17:21:08 -0800 (Mon, 05 Jan 2004)
Revision: 5223
Log message:

      Fixed the primitive rules with their computational contents.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-05 18:02:28 -0800 (Mon, 05 Jan 2004)
Revision: 5224
Log message:

      Fixed some computational contents in some primitive rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-05 18:26:38 -0800 (Mon, 05 Jan 2004)
Revision: 5225
Log message:

      Scripts for getting the "grounded" status of proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-05 21:14:32 -0800 (Mon, 05 Jan 2004)
Revision: 5226
Log message:

      One of the rules already had a proof and does not need to be an axiom.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-06 14:49:36 -0800 (Tue, 06 Jan 2004)
Revision: 5227
Log message:

      - Proved the reduce_ycomb and reduce_fix rewrites.
      - %.ppo depends on %.cmiz (imagine, for example, replacing val with topval in .mli).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-06 15:10:51 -0800 (Tue, 06 Jan 2004)
Revision: 5228
Log message:

      When omake is present (in /usr/bin or /usr/local/bin), use it even when
      .omakedb is not there.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-06 20:38:54 -0800 (Tue, 06 Jan 2004)
Revision: 5229
Log message:

      Cleaned up exception reporting a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-06 21:49:24 -0800 (Tue, 06 Jan 2004)
Revision: 5230
Log message:

      - Do not catch exceptions when running with OCAMLRUNPARAM=b.
      - reflib does not use macros and does not need to be preprocessed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-06 23:43:07 -0800 (Tue, 06 Jan 2004)
Revision: 5231
Log message:

      Minor code clean-up.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-06 23:43:22 -0800 (Tue, 06 Jan 2004)
Revision: 5232
Log message:

      My definition of rings.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-07 18:14:28 -0800 (Wed, 07 Jan 2004)
Revision: 5235
Log message:

       - Defined subring.
       - Added more ring examples.
      
       Notes:
         1. The typeinf_resource for as_additive needs work.
         2. The ring of even integers is commented out since for now
            we don't have enough axioms for the "rem" operation.
            I would appreciate if Yegor can add it( and incorporate it
            into arithT).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-07 22:01:19 -0800 (Wed, 07 Jan 2004)
Revision: 5236
Log message:

      Posting full version of my thesis ("tech report edition") online.
      

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

      Partial fix of the profiling code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-08 17:07:04 -0800 (Thu, 08 Jan 2004)
Revision: 5238
Log message:

      Cleaned up some of the set code in JProver. This gives about 5% speedup
      on the "status_all".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-08 19:32:14 -0800 (Thu, 08 Jan 2004)
Revision: 5239
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 N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-08 22:36:14 -0800 (Thu, 08 Jan 2004)
Revision: 5240
Log message:

      Itt_bool - added commutativity of band
      Itt_order - all properties up to strict/unstrict total order (decidable).
      Inverse order, conversion between strict-unstrict orders, their mutual
      relations, they preserve total orderness.
      lt_bool, le_bool, gt_bool and ge_bool are total orders over integers.
      Lots of trivial things are not proved but interesting theorems are.
      Record wrappers probably should be moved to a separate file.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-09 23:55:35 -0800 (Fri, 09 Jan 2004)
Revision: 5241
Log message:

      Itt_bool - boolMoveToConcl moves from assert to assert.
      Itt_order.mli - almost nothing was exposed
      Itt_rat - first steps based on itt_field and itt_order.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2004-01-10 16:57:39 -0800 (Sat, 10 Jan 2004)
Revision: 5242
Log message:

      Restored "==" (instead of "=") for bound variables.
      It was removed by mistake in revision 1.5
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-10 23:32:54 -0800 (Sat, 10 Jan 2004)
Revision: 5243
Log message:

      quotient - quotientElimination2 didn't have subgoal labels
      bool - boolMoveToConcl in a little general form
      int_ext - boolean equality can be multiplied by non-zero integer
      order - some tune-up of intro/elim resources
      rat - proved some theorems
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-11 23:37:48 -0800 (Sun, 11 Jan 2004)
Revision: 5244
Log message:

      Some more progress.
      At /itt_rat/ratEquality/1 if I apply "dT 0 twa" (or anything automatic after dT 0)
      metaprl does not terminate. Do resources allow non-terminating scenarios?
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-12 21:12:32 -0800 (Mon, 12 Jan 2004)
Revision: 5245
Log message:

      Rationals are totally ordered (<) - proved.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-12 21:21:45 -0800 (Mon, 12 Jan 2004)
Revision: 5246
Log message:

      unsubstantial changes I forgot to submit much earlier.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-12 21:29:35 -0800 (Mon, 12 Jan 2004)
Revision: 5247
Log message:

      One more minor update
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-13 17:40:51 -0800 (Tue, 13 Jan 2004)
Revision: 5248
Log message:

      Fixing a bug in normalizeC that caused stack overflow in some cases.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-13 21:35:13 -0800 (Tue, 13 Jan 2004)
Revision: 5249
Log message:

      Extending definitions of div and rem to negative integers,
      hopefully it's correct.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-14 00:08:17 -0800 (Wed, 14 Jan 2004)
Revision: 5250
Log message:

      Field implementation.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-14 13:39:29 -0800 (Wed, 14 Jan 2004)
Revision: 5251
Log message:

      Fixed a broken proof step caused by the removal of Itt_group!isCommutative_wf.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-14 22:38:11 -0800 (Wed, 14 Jan 2004)
Revision: 5252
Log message:

      itt_order - min,max added
      itt_rat - less-or-equal added
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-16 17:41:05 -0800 (Fri, 16 Jan 2004)
Revision: 5253
Log message:

      Uncommented the ring of even integers part.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-16 21:07:34 -0800 (Fri, 16 Jan 2004)
Revision: 5254
Log message:

      Give summary of ungrounded dependencies.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-17 14:17:16 -0800 (Sat, 17 Jan 2004)
Revision: 5255
Log message:

      Fully grounded proof of /itt_record_label0/decide_eq_label
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-17 14:34:32 -0800 (Sat, 17 Jan 2004)
Revision: 5256
Log message:

      Forgot to commit the actual proof.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-17 15:11:41 -0800 (Sat, 17 Jan 2004)
Revision: 5257
Log message:

      Finished the proofs in Itt_record_label0 theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-17 17:19:52 -0800 (Sat, 17 Jan 2004)
Revision: 5258
Log message:

      Some progress on itt_nat proofs.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-17 21:11:08 -0800 (Sat, 17 Jan 2004)
Revision: 5259
Log message:

      natBackInduction - proved.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-17 21:56:21 -0800 (Sat, 17 Jan 2004)
Revision: 5260
Log message:

      Shorter proof.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-01-18 17:47:06 -0800 (Sun, 18 Jan 2004)
Revision: 5261
Log message:

      Finish the proof of /itt_record/recordEliminationL.
      
      Fix itt_pointwise/hypSubstPointwis rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-18 18:54:46 -0800 (Sun, 18 Jan 2004)
Revision: 5262
Log message:

      Finished some of the proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-18 21:20:15 -0800 (Sun, 18 Jan 2004)
Revision: 5263
Log message:

      Use Yegor's new taa/twa suffixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-19 11:26:27 -0800 (Mon, 19 Jan 2004)
Revision: 5264
Log message:

      Pay attention to OCAMLLIB variable, not just CAMLLIB.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-20 17:17:09 -0800 (Tue, 20 Jan 2004)
Revision: 5265
Log message:

      Defined unit ring.
      
      Note: There might be a better way to formalize "isUnit" and the theorem
            "the set of units forms a group under multiplication."
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-20 22:26:07 -0800 (Tue, 20 Jan 2004)
Revision: 5266
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: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-21 00:42:51 -0800 (Wed, 21 Jan 2004)
Revision: 5267
Log message:

      Re-formalized the theorem "The set of units forms a group under multiplication."
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-01-21 16:29:08 -0800 (Wed, 21 Jan 2004)
Revision: 5268
Log message:

      Changed the meta_term and hypothesis type definitions in term_sig
      to avoid type duplication.
      
      The new type definitions are toplevel as polymorphic types.  For example
      
      |   type 'term poly_hypothesis = Hypothesis of 'term | ...
      
      Then, once the term type is defined, we can use the following
      definition:
      
      |   type hypothesis = term poly_hypothesis
      
      This is in preparation for extending the hypothesis type with
      cases for recursive sequents.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-21 22:08:47 -0800 (Wed, 21 Jan 2004)
Revision: 5269
Log message:

      - Adding the MESA theory to "THEORIES=all"
      - Adding an anchor to the "Simplified syntax" section of mp-terms.html
      - Other minor fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-22 15:04:48 -0800 (Thu, 22 Jan 2004)
Revision: 5270
Log message:

      - Added omake support to theories/kat
      - For now, do not include kat and mesa in THEORIES=all (and nightly status checks) -
      they are pretty big theories, but do not have much proofs yet.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-22 16:03:18 -0800 (Thu, 22 Jan 2004)
Revision: 5271
Log message:

      - In the previous commit, forgot to actually drop mesa and kat theories
      from the list
      
      - Removing couple of unused files.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-23 00:37:20 -0800 (Fri, 23 Jan 2004)
Revision: 5272
Log message:

      Added concepts in polynomial theory.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-23 10:30:56 -0800 (Fri, 23 Jan 2004)
Revision: 5273
Log message:

      Forgot .prla file.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-24 21:41:30 -0800 (Sat, 24 Jan 2004)
Revision: 5274
Log message:

      Added rat{'a;'b} wrapper for ('a,'b) (stands for a/b), I think it's better than just plain ('a,'b).
      
      Do you think "rat" is ok or it does not sound good and I'd better use "ratio"?
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-25 01:41:18 -0800 (Sun, 25 Jan 2004)
Revision: 5275
Log message:

      More about polynomials.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 01:00:53 -0800 (Mon, 26 Jan 2004)
Revision: 5276
Log message:

      Use "-inline 3" when compiling to native code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 01:00:53 -0800 (Mon, 26 Jan 2004)
Revision: 5277
Log message:

      Use "-inline 3" when compiling to native code.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-26 02:02:23 -0800 (Mon, 26 Jan 2004)
Revision: 5278
Log message:

      More about poly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 04:49:21 -0800 (Mon, 26 Jan 2004)
Revision: 5279
Log message:

      Better error printing:
       - when makeFoldC fails.
       - when a building a MetaPRL item (rule, rewrite, etc) fails.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 04:55:48 -0800 (Mon, 26 Jan 2004)
Revision: 5280
Log message:

      Use bind instead of lambda for marking SO variables in rule arguments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 05:43:00 -0800 (Mon, 26 Jan 2004)
Revision: 5281
Log message:

      Some progress towards proper definitions for itt_poly operations. Some proofs
      are still incomplete - we need a stronger indEqual (see my post in the newsgroup)
      to finish those proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 06:59:36 -0800 (Mon, 26 Jan 2004)
Revision: 5282
Log message:

      int_sqequalC now takes << 'a ~ 'b >> as an argument - this makes it much easier
      to specify what exactly we want to substitute.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 15:12:39 -0800 (Mon, 26 Jan 2004)
Revision: 5283
Log message:

      - Added a genT tactic for generalizing the conclusion.
      - Simplified some of the proofs in itt_fset.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-26 16:07:41 -0800 (Mon, 26 Jan 2004)
Revision: 5284
Log message:

      Broken proof fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 19:11:17 -0800 (Mon, 26 Jan 2004)
Revision: 5285
Log message:

      Replaced the Itt_int_base.indEquality axiom with a stronger derived rule
      and used it to prove Itt_nat.indEquality.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-26 19:39:57 -0800 (Mon, 26 Jan 2004)
Revision: 5286
Log message:

      Re-defined eval_poly
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-26 19:56:16 -0800 (Mon, 26 Jan 2004)
Revision: 5287
Log message:

      Redefined group_power with "define" instead of "declare" and "prim_rw".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 23:08:13 -0800 (Mon, 26 Jan 2004)
Revision: 5288
Log message:

      - The Itt_antiquotient.eq_mem_eq rule was missing an assumption, fixed.
      - Fixed a few broken links in htmlman
      - Started a theory implementing a "base" type idea that I've posted to the
      newsgroup about a month ago.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-27 02:19:19 -0800 (Tue, 27 Jan 2004)
Revision: 5289
Log message:

      More progress on proving..
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-27 14:25:22 -0800 (Tue, 27 Jan 2004)
Revision: 5290
Log message:

      License should not be a part of the doc.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-27 14:59:07 -0800 (Tue, 27 Jan 2004)
Revision: 5291
Log message:

      Omake used to produce the list of theories to put into the .pdf file by doing
      
      ALL_THEORIES = $(intersection $(DEF_ALL_THEORIES), $(THEORIES))
      
      Unfortunately, $intersection puts everything in alphabetical order, which is
      unacceptable (e.g. czf must go after itt). I changed it to simply use
      the standard list of theories (which will fail if some of those theories are not
      in $(THEORIES) ).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-27 18:08:49 -0800 (Tue, 27 Jan 2004)
Revision: 5292
Log message:

      Re-defined eval_poly.
      

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

      Proved a number of facts about min and max.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-27 19:32:38 -0800 (Tue, 27 Jan 2004)
Revision: 5294
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: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-27 20:43:23 -0800 (Tue, 27 Jan 2004)
Revision: 5295
Log message:

      Itt_int_ext, Itt_rat - inequalities over constants added to reduce,intro and elim resources.
      Itt_rat - some properties of >= stated.
      Itt_supinf - it can partly prove what it has to, check test2 for example,
      all remaining subgoals are massaged hyps.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-27 22:06:33 -0800 (Tue, 27 Jan 2004)
Revision: 5296
Log message:

      - When the list of subgoals is too long, show at least the first 5
      (I am not sure about the constants 5 and 20, may be they should be bigger. And
      ideally they should be configurable...).
      
      - Added a debug variable that would force printing the full list of subgoals,
      even when it is very long.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-27 23:40:34 -0800 (Tue, 27 Jan 2004)
Revision: 5297
Log message:

      - Better error reporting in filter
      - Better detection of MP items with duplicate names.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 01:32:43 -0800 (Wed, 28 Jan 2004)
Revision: 5298
Log message:

      Made trivialT a bit smarter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 02:17:28 -0800 (Wed, 28 Jan 2004)
Revision: 5299
Log message:

      A bit more progress in the eq_base theory.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-28 02:42:01 -0800 (Wed, 28 Jan 2004)
Revision: 5300
Log message:

      Defined Integral Domain.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 02:50:01 -0800 (Wed, 28 Jan 2004)
Revision: 5301
Log message:

      Minor clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 03:12:14 -0800 (Wed, 28 Jan 2004)
Revision: 5302
Log message:

      Added a Sequent.all_hyps function that returns a list of all hypothesis in
      the goal sequent.
      

Changes by: ( at unknown.email)
Date: 2004-01-28 03:15:41 -0800 (Wed, 28 Jan 2004)
Revision: 5303
Log message:

      This commit was manufactured by cvs2svn to create branch
      'recursive_sequents'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 03:15:41 -0800 (Wed, 28 Jan 2004)
Revision: 5304
Log message:

      Recursive sequents - changing the definition of the "hypothesis" type.
      
      THis is a first (very small) step towards implementing recursive
      sequents. Tomorrow Nathan will post a description of what we are planning
      to implement.
      

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

      Typo - no sure how this got in here.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 12:00:08 -0800 (Wed, 28 Jan 2004)
Revision: 5306
Log message:

      Adding support for native code profiling to omake.
      

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

      Removed all the unused "open" statements.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-28 20:40:29 -0800 (Wed, 28 Jan 2004)
Revision: 5308
Log message:

      Clean-ups.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 21:06:59 -0800 (Wed, 28 Jan 2004)
Revision: 5309
Log message:

      No longer need to put (or allowed to put) the last sequent context into
      the list of rule/rewrite arguments, even when there are non-context hypotheses
      after that.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-28 22:20:25 -0800 (Wed, 28 Jan 2004)
Revision: 5310
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: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 22:42:43 -0800 (Wed, 28 Jan 2004)
Revision: 5311
Log message:

      Better and more complete error-detection and reporting in the code I've
      checked in in my previous commit.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-29 00:22:39 -0800 (Thu, 29 Jan 2004)
Revision: 5312
Log message:

      Defined ring, commutative unitring, integral domain, and field with
      decidable equality.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-29 01:37:29 -0800 (Thu, 29 Jan 2004)
Revision: 5313
Log message:

      Forgot this file.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-29 01:52:40 -0800 (Thu, 29 Jan 2004)
Revision: 5314
Log message:

      Clean-up.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-29 02:18:31 -0800 (Thu, 29 Jan 2004)
Revision: 5315
Log message:

      Changed file names to conform to the naming convention.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-29 10:51:01 -0800 (Thu, 29 Jan 2004)
Revision: 5316
Log message:

      Proper solution for the out-of-order theories problem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-29 19:00:46 -0800 (Thu, 29 Jan 2004)
Revision: 5317
Log message:

      In band and bimplies, the second operand only needs to be in bool
      when the first one is true.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-29 22:59:05 -0800 (Thu, 29 Jan 2004)
Revision: 5318
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-30 00:02:04 -0800 (Fri, 30 Jan 2004)
Revision: 5319
Log message:

      Changed anyArithRel2geT to use derived rules instead of tactics.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-30 04:46:54 -0800 (Fri, 30 Jan 2004)
Revision: 5320
Log message:

      More about polynomials.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-30 10:34:23 -0800 (Fri, 30 Jan 2004)
Revision: 5321
Log message:

      Finished the proof of the last rewrite, simplified the proof of sum_wf.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-30 13:36:23 -0800 (Fri, 30 Jan 2004)
Revision: 5322
Log message:

      Fixing a few proofs that were broken by a recent commit.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-31 10:06:43 -0800 (Sat, 31 Jan 2004)
Revision: 5324
Log message:

      Some improvements, after this I'm going to try a little different approach
      for proof-support part of SupInf
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-31 19:41:30 -0800 (Sat, 31 Jan 2004)
Revision: 5325
Log message:

      Some improvements
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-31 23:02:08 -0800 (Sat, 31 Jan 2004)
Revision: 5326
Log message:

      Covered almost everything - one case is not covered in "test",
      there is one verbose way to cover it but I'll try to make it more concise.