[nogin] _ Since OCaml ints are 31_bit on 32_bit platform, constats like 0x89ac12bd and_ Mon Sep 19 05:26:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-01-961202000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-01-961202000-PDT.html [nogin] When using omake, explicitly call for editor/ml/mp.opt_ Mon Sep 19 05:26:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-02-489533000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-02-489533000-PDT.html [nogin] Fixing couple of unescaped backslashes._ Mon Sep 19 05:26:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-02-853856000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-02-853856000-PDT.html [xiny] Changed according axioms to be primitive._ Mon Sep 19 05:26:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-03-408750000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-03-408750000-PDT.html [xiny] Fixed the primitive rules with their computational contents._ Mon Sep 19 05:26:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-04-232255000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-04-232255000-PDT.html [xiny] Fixed some computational contents in some primitive rules._ Mon Sep 19 05:26:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-04-755645000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-04-755645000-PDT.html [nogin] Scripts for getting the _grounded_ status of proofs._ Mon Sep 19 05:26:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-05-156735000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-05-156735000-PDT.html [nogin] One of the rules already had a proof and does not need to be an axiom._ Mon Sep 19 05:26:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-05-588370000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-05-588370000-PDT.html [nogin] _ Proved the reduce_ycomb and reduce_fix rewrites._ Mon Sep 19 05:26:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-06-009879000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-06-009879000-PDT.html [nogin] When omake is present _in /usr/bin or /usr/local/bin_, use it even when_ Mon Sep 19 05:26:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-11-808329000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-11-808329000-PDT.html [nogin] Cleaned up exception reporting a bit._ Mon Sep 19 05:26:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-12-180802000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-12-180802000-PDT.html [nogin] _ Do not catch exceptions when running with OCAMLRUNPARAM_b._ Mon Sep 19 05:26:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-12-849490000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-12-849490000-PDT.html [nogin] Minor code clean_up._ Mon Sep 19 05:26:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-13-233661000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-13-233661000-PDT.html [xiny] My definition of rings._ Mon Sep 19 05:26:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-13-681074000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-26-13-681074000-PDT.html [xiny] _ Defined subring._ Mon Sep 19 05:27:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-11-452495000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-11-452495000-PDT.html [nogin] Posting full version of my thesis __tech report edition__ online._ Mon Sep 19 05:27:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-32-410726000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-32-410726000-PDT.html [nogin] Partial fix of the profiling code._ Mon Sep 19 05:27:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-32-912280000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-32-912280000-PDT.html [nogin] Cleaned up some of the set code in JProver. This gives about 5_ speedup_ Mon Sep 19 05:27:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-33-275940000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-33-275940000-PDT.html [nogin] When comparing symbols, compare ints first, instead of using Pervasives.compare_ Mon Sep 19 05:27:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-33-934428000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-33-934428000-PDT.html [yegor] Itt_bool _ added commutativity of band_ Mon Sep 19 05:27:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-34-513864000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-34-513864000-PDT.html [yegor] Itt_bool _ boolMoveToConcl moves from assert to assert._ Mon Sep 19 05:27:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-40-285256000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-40-285256000-PDT.html [krupski] Restored ____ _instead of ____ for bound variables._ Mon Sep 19 05:27:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-43-406502000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-43-406502000-PDT.html [yegor] quotient _ quotientElimination2 didn_t have subgoal labels_ Mon Sep 19 05:27:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-43-781198000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-43-781198000-PDT.html [yegor] Some more progress._ Mon Sep 19 05:27:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-59-313952000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-27-59-313952000-PDT.html [yegor] Rationals are totally ordered ___ _ proved._ Mon Sep 19 05:28:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-00-678914000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-00-678914000-PDT.html [yegor] unsubstantial changes I forgot to submit much earlier._ Mon Sep 19 05:28:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-03-489445000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-03-489445000-PDT.html [yegor] One more minor update_ Mon Sep 19 05:28:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-06-973830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-06-973830000-PDT.html [yegor] Fixing a bug in normalizeC that caused stack overflow in some cases._ Mon Sep 19 05:28:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-07-652408000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-07-652408000-PDT.html [yegor] Extending definitions of div and rem to negative integers,_ Mon Sep 19 05:28:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-09-438715000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-09-438715000-PDT.html [xiny] Field implementation._ Mon Sep 19 05:28:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-09-900828000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-09-900828000-PDT.html [xiny] Fixed a broken proof step caused by the removal of Itt_group_isCommutative_wf._ Mon Sep 19 05:28:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-48-347576000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-48-347576000-PDT.html [yegor] itt_order _ min,max added_ Mon Sep 19 05:28:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-57-018563000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-28-57-018563000-PDT.html [xiny] Uncommented the ring of even integers part._ Mon Sep 19 05:29:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-29-08-962814000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-29-08-962814000-PDT.html [nogin] Give summary of ungrounded dependencies._ Mon Sep 19 05:29:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-29-21-020323000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-29-21-020323000-PDT.html [nogin] Fully grounded proof of /itt_record_label0/decide_eq_label_ Mon Sep 19 05:29:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-29-21-377966000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-29-21-377966000-PDT.html [nogin] Forgot to commit the actual proof._ Mon Sep 19 05:31:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-00-807462000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-00-807462000-PDT.html [nogin] Finished the proofs in Itt_record_label0 theory._ Mon Sep 19 05:31:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-02-056294000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-02-056294000-PDT.html [nogin] Some progress on itt_nat proofs._ Mon Sep 19 05:31:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-03-137706000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-03-137706000-PDT.html [yegor] natBackInduction _ proved._ Mon Sep 19 05:31:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-05-053015000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-05-053015000-PDT.html [nogin] Shorter proof._ Mon Sep 19 05:31:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-07-180952000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-07-180952000-PDT.html [kopylov] Finish the proof of /itt_record/recordEliminationL._ Mon Sep 19 05:31:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-10-284233000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-10-284233000-PDT.html [nogin] Finished some of the proofs._ Mon Sep 19 05:31:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-11-096472000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-11-096472000-PDT.html [nogin] Use Yegor_s new taa/twa suffixes._ Mon Sep 19 05:31:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-12-296870000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-12-296870000-PDT.html [nogin] Pay attention to OCAMLLIB variable, not just CAMLLIB._ Mon Sep 19 05:31:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-16-194916000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-16-194916000-PDT.html [xiny] Defined unit ring._ Mon Sep 19 05:31:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-16-553582000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-16-553582000-PDT.html [yegor] 1.deletemax added to splay_table _and other tables_._ Mon Sep 19 05:31:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-19-900983000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-19-900983000-PDT.html [xiny] Re_formalized the theorem _The set of units forms a group under multiplication.__ Mon Sep 19 05:31:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-28-496578000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-28-496578000-PDT.html [jyh] Changed the meta_term and hypothesis type definitions in term_sig_ Mon Sep 19 05:31:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-32-576042000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-32-576042000-PDT.html [nogin] _ Adding the MESA theory to _THEORIES_all__ Mon Sep 19 05:31:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-34-680267000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-34-680267000-PDT.html [nogin] _ Added omake support to theories/kat_ Mon Sep 19 05:31:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-35-336572000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-35-336572000-PDT.html [nogin] _ In the previous commit, forgot to actually drop mesa and kat theories_ Mon Sep 19 05:31:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-35-782908000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-35-782908000-PDT.html [xiny] Added concepts in polynomial theory._ Mon Sep 19 05:31:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-36-321153000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-36-321153000-PDT.html [xiny] Forgot .prla file._ Mon Sep 19 05:31:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-36-987571000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-36-987571000-PDT.html [yegor] Added rat__a__b_ wrapper for __a,_b_ _stands for a/b_, I think it_s better than just plain __a,_b_._ Mon Sep 19 05:31:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-39-744115000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-39-744115000-PDT.html [xiny] More about polynomials._ Mon Sep 19 05:31:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-44-725155000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-44-725155000-PDT.html [nogin] Use __inline 3_ when compiling to native code._ Mon Sep 19 05:31:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-56-446830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-56-446830000-PDT.html [nogin] Use __inline 3_ when compiling to native code._ Mon Sep 19 05:31:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-56-883112000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-56-883112000-PDT.html [xiny] More about poly._ Mon Sep 19 05:31:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-57-254480000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-31-57-254480000-PDT.html [nogin] Better error printing__ Mon Sep 19 05:34:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-17-716235000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-17-716235000-PDT.html [nogin] Use bind instead of lambda for marking SO variables in rule arguments._ Mon Sep 19 05:34:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-18-482104000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-18-482104000-PDT.html [nogin] Some progress towards proper definitions for itt_poly operations. Some proofs_ Mon Sep 19 05:34:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-25-138244000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-25-138244000-PDT.html [nogin] int_sqequalC now takes __ _a _ _b __ as an argument _ this makes it much easier_ Mon Sep 19 05:34:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-33-403192000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-33-403192000-PDT.html [nogin] _ Added a genT tactic for generalizing the conclusion._ Mon Sep 19 05:34:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-40-233839000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-34-40-233839000-PDT.html [xiny] Broken proof fix._ Mon Sep 19 05:36:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-36-15-563347000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-36-15-563347000-PDT.html [nogin] Replaced the Itt_int_base.indEquality axiom with a stronger derived rule_ Mon Sep 19 05:36:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-36-17-600120000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-36-17-600120000-PDT.html [xiny] Re_defined eval_poly_ Mon Sep 19 05:37:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-37-618807000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-37-618807000-PDT.html [xiny] Redefined group_power with _define_ instead of _declare_ and _prim_rw_._ Mon Sep 19 05:37:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-38-038413000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-38-038413000-PDT.html [nogin] _ The Itt_antiquotient.eq_mem_eq rule was missing an assumption, fixed._ Mon Sep 19 05:37:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-40-801192000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-40-801192000-PDT.html [xiny] More progress on proving.._ Mon Sep 19 05:37:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-42-700492000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-42-700492000-PDT.html [nogin] License should not be a part of the doc._ Mon Sep 19 05:37:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-50-980250000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-50-980250000-PDT.html [nogin] Omake used to produce the list of theories to put into the .pdf file by doing_ Mon Sep 19 05:37:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-51-367570000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-51-367570000-PDT.html [xiny] Re_defined eval_poly._ Mon Sep 19 05:37:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-51-762841000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-51-762841000-PDT.html [nogin] Proved a number of facts about min and max._ Mon Sep 19 05:37:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-53-781837000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-53-781837000-PDT.html [nogin] _ Made Lm_list_util.flat_map tail_recursive._ Mon Sep 19 05:37:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-56-014763000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-56-014763000-PDT.html [yegor] Itt_int_ext, Itt_rat _ inequalities over constants added to reduce,intro and elim resources._ Mon Sep 19 05:37:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-56-429657000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-37-56-429657000-PDT.html [nogin] _ When the list of subgoals is too long, show at least the first 5_ Mon Sep 19 05:40:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-51-899447000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-51-899447000-PDT.html [nogin] _ Better error reporting in filter_ Mon Sep 19 05:40:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-52-316348000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-52-316348000-PDT.html [nogin] Made trivialT a bit smarter._ Mon Sep 19 05:40:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-52-859357000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-52-859357000-PDT.html [nogin] A bit more progress in the eq_base theory._ Mon Sep 19 05:40:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-53-257288000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-53-257288000-PDT.html [xiny] Defined Integral Domain._ Mon Sep 19 05:40:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-54-207032000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-40-54-207032000-PDT.html [nogin] Minor clean_up._ Mon Sep 19 05:41:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-41-11-634432000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-41-11-634432000-PDT.html [nogin] Added a Sequent.all_hyps function that returns a list of all hypothesis in_ Mon Sep 19 05:41:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-41-12-077027000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-41-12-077027000-PDT.html [] This commit was manufactured by cvs2svn to create branch_ Mon Sep 19 05:41:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-41-12-592994000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-41-12-592994000-PDT.html [nogin] Recursive sequents _ changing the definition of the _hypothesis_ type._ Mon Sep 19 05:43:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-56-533422000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-56-533422000-PDT.html [nogin] Typo _ no sure how this got in here._ Mon Sep 19 05:43:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-57-055634000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-57-055634000-PDT.html [nogin] Adding support for native code profiling to omake._ Mon Sep 19 05:43:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-57-448327000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-57-448327000-PDT.html [nogin] Removed all the unused _open_ statements._ Mon Sep 19 05:43:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-58-110494000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-58-110494000-PDT.html [xiny] Clean_ups._ Mon Sep 19 05:43:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-59-957392000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-43-59-957392000-PDT.html [nogin] No longer need to put _or allowed to put_ the last sequent context into_ Mon Sep 19 05:44:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-44-47-081664000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-44-47-081664000-PDT.html [yegor] Lm_splay_table, etc _ list_of added,_ Mon Sep 19 05:44:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-44-48-542428000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-44-48-542428000-PDT.html [nogin] Better and more complete error_detection and reporting in the code I_ve_ Mon Sep 19 05:48:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-28-378536000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-28-378536000-PDT.html [xiny] Defined ring, commutative unitring, integral domain, and field with_ Mon Sep 19 05:48:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-28-841240000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-28-841240000-PDT.html [xiny] Forgot this file._ Mon Sep 19 05:48:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-36-582971000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-36-582971000-PDT.html [xiny] Clean_up._ Mon Sep 19 05:48:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-37-073504000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-37-073504000-PDT.html [xiny] Changed file names to conform to the naming convention._ Mon Sep 19 05:48:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-51-230551000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-48-51-230551000-PDT.html [nogin] Proper solution for the out_of_order theories problem._ Mon Sep 19 05:49:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-06-446496000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-06-446496000-PDT.html [nogin] In band and bimplies, the second operand only needs to be in bool_ Mon Sep 19 05:49:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-06-847219000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-06-847219000-PDT.html [yegor] Lm_splay_table _ more efficient implementation of list_of._ Mon Sep 19 05:49:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-12-589230000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-12-589230000-PDT.html [nogin] Changed anyArithRel2geT to use derived rules instead of tactics._ Mon Sep 19 05:49:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-13-203354000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-13-203354000-PDT.html [xiny] More about polynomials._ Mon Sep 19 05:49:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-58-314557000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-49-58-314557000-PDT.html [nogin] Finished the proof of the last rewrite, simplified the proof of sum_wf._ Mon Sep 19 05:50:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-41-790283000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-41-790283000-PDT.html [nogin] Fixing a few proofs that were broken by a recent commit._ Mon Sep 19 05:50:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-44-045351000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-44-045351000-PDT.html [yegor] Some improvements, after this I_m going to try a little different approach_ Mon Sep 19 05:50:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-47-733724000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-47-733724000-PDT.html [yegor] Some improvements_ Mon Sep 19 05:50:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-48-332585000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-48-332585000-PDT.html [yegor] Covered almost everything _ one case is not covered in _test_,_ Mon Sep 19 05:50:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-48-954867000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-01/2005-09-19-05-50-48-954867000-PDT.html