[yegor] working on phases 1 and 2_Wed Jul 2 13:36:06 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-02-13-36-06-577927000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-02-13-36-06-577927000-PDT.html[yegor] added box_to_right rule to phase 1_Thu Jul 3 14:02:13 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-03-14-02-13-457531000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-03-14-02-13-457531000-PDT.html[yegor] first draft of phase 1 finished_Fri Jul 4 11:22:53 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-04-11-22-53-695006000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-04-11-22-53-695006000-PDT.html[yegor] all phases finished in first draft, it compiles but never executed yet_Sat Jul 5 12:54:58 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-05-12-54-58-804096000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-05-12-54-58-804096000-PDT.html[yegor] compiles, runs and even checks up for self_referencial example._Tue Jul 8 18:07:05 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-08-18-07-05-618053000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-08-18-07-05-618053000-PDT.html[yegor] Changed the families handling code because merging of families was incorrectly implemented. It used to be amp from representatives to the whole family, but if you think even a bit, you_ll realize that it can_t work. Now it_s a set _list_ of sets _families_, not very efficient but can be replaced with an ordered set with a natural_lexicographical_ order on families._Wed Jul 9 19:32:10 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-09-19-32-10-533927000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-09-19-32-10-533927000-PDT.html[jyh] More progress on camlp4. I wish they would document the quotation syntax somewhere__Thu Jul 10 12:50:32 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-12-50-32-682569000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-12-50-32-682569000-PDT.html[yegor] added phase1_2 substitution between families computation _assign_ and realization per se _g2h__Thu Jul 10 13:33:52 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-13-33-52-136194000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-13-33-52-136194000-PDT.html[jyh] More progress in filter_ocaml, still a ways to go._Thu Jul 10 16:40:55 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-16-40-55-062540000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-16-40-55-062540000-PDT.html[yegor] Added some code that extracts and prints all formulas that were claimed tautologies _and left unproven_ in the proof._Thu Jul 10 19:30:09 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-19-30-09-323042000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-19-30-09-323042000-PDT.html[jyh] Ported patterns._Thu Jul 10 20:33:35 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-20-33-35-272845000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-10-20-33-35-272845000-PDT.html[jyh] Halfway through types, lots of work to do._Fri Jul 11 12:36:06 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-11-12-36-06-878135000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-11-12-36-06-878135000-PDT.html[jyh] Updated sig_item._Fri Jul 11 14:44:11 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-11-14-44-11-235176000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-11-14-44-11-235176000-PDT.html[jyh] Part way through str_item_Fri Jul 11 14:52:12 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-11-14-52-12-543922000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-11-14-52-12-543922000-PDT.html[yegor] added connection with JProver._Sun Jul 13 12:38:25 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-13-12-38-25-240571000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-13-12-38-25-240571000-PDT.html[yegor] a tiny simplification_Sun Jul 13 15:09:56 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-13-15-09-56-911717000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-13-15-09-56-911717000-PDT.html[jyh] filter_ocaml.ml now almost compiles. Except, the compiler keeps complaining that_Mon Jul 14 14:29:26 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-14-29-26-799260000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-14-29-26-799260000-PDT.html[jyh] Hoist some definitions out of the big recursive definition, and it compiles._Mon Jul 14 14:45:33 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-14-45-33-582350000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-14-45-33-582350000-PDT.html[jyh] Filter compiles and runs, but we get this__Mon Jul 14 15:28:55 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-15-28-55-484122000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-15-28-55-484122000-PDT.html[yegor] eliminated explicit references to axiom indices and arithmetic over them _where necessitation was needed__Mon Jul 14 17:42:48 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-17-42-48-212052000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-17-42-48-212052000-PDT.html[yegor] Added Nec rule, in its generic _not restricted to axioms_ form._Mon Jul 14 19:07:59 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-19-07-59-152283000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-19-07-59-152283000-PDT.html[jyh] New Campl4 uses an undocumented scheme for the printers, that I_Mon Jul 14 19:13:20 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-19-13-20-795776000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-19-13-20-795776000-PDT.html[yegor] more progress towards multi_modal case_Mon Jul 14 20:56:31 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-20-56-31-300507000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-14-20-56-31-300507000-PDT.html[jyh] Finally, all the basic stuff is port to Camlp4 3.10._Tue Jul 15 19:17:15 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-15-19-17-15-857087000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-15-19-17-15-857087000-PDT.html[yegor] Added AndRight rule and it exposed an error g2h code for BoxRight _lemma3 was implemented incorrectly and worked only for one hypothesis_._Tue Jul 15 22:05:37 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-15-22-05-37-692604000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-15-22-05-37-692604000-PDT.html[yegor] added AndLeft_Wed Jul 16 08:54:45 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-08-54-45-834038000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-08-54-45-834038000-PDT.html[yegor] forgot to add these files a couple of days ago_Wed Jul 16 08:55:44 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-08-55-44-419628000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-08-55-44-419628000-PDT.html[yegor] added OrLeft_Wed Jul 16 09:26:51 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-09-26-51-162533000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-09-26-51-162533000-PDT.html[yegor] OrRight added_Wed Jul 16 09:55:24 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-09-55-24-851375000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-09-55-24-851375000-PDT.html[jyh] _Almost_ compiles with 3.10. Term errors during .prla parsing are warnings only._Wed Jul 16 13:09:42 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-13-09-42-236028000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-13-09-42-236028000-PDT.html[yegor] added NegRight._Wed Jul 16 14:09:41 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-14-09-41-830179000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-14-09-41-830179000-PDT.html[jyh] Compiles with OCaml 3.10 _using omake 0.9.9_._Wed Jul 16 14:41:11 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-14-41-11-049811000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-14-41-11-049811000-PDT.html[jyh] Fix all the theory files._Wed Jul 16 15:50:33 PDT 2008
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-15-50-33-927104000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2008-07/2008-07-16-15-50-33-927104000-PDT.html