[yegor] One more list converted to map_Mon Sep 19 07:37:51 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-37-51-393903000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-37-51-393903000-PDT.html[yegor] another sets turned to map_Mon Sep 19 07:37:51 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-37-52-004171000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-37-52-004171000-PDT.html[nogin] More comment formatting. Now every toplevel _doc_ item has an _implicit__Mon Sep 19 07:37:52 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-37-52-554682000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-37-52-554682000-PDT.html[nogin] The MMC part of the previous commit_Mon Sep 19 07:38:08 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-08-913784000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-08-913784000-PDT.html[yegor] one more list converted to set_Mon Sep 19 07:38:10 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-10-340716000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-10-340716000-PDT.html[yegor] another set instead a list_Mon Sep 19 07:38:10 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-10-854601000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-10-854601000-PDT.html[nogin] When reporting an interface ___ implementation mismatch, give the loc of the_Mon Sep 19 07:38:11 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-11-527410000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-11-527410000-PDT.html[yegor] more lists converted to maps_Mon Sep 19 07:38:12 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-12-086935000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-12-086935000-PDT.html[yegor] one more set instead of list_Mon Sep 19 07:38:12 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-12-828811000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-12-828811000-PDT.html[yegor] more sets_Mon Sep 19 07:38:13 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-13-337748000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-13-337748000-PDT.html[yegor] and more sets_Mon Sep 19 07:38:13 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-13-929332000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-13-929332000-PDT.html[yegor] more maps_Mon Sep 19 07:38:14 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-14-494512000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-14-494512000-PDT.html[yegor] more sets_Mon Sep 19 07:38:15 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-15-028391000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-15-028391000-PDT.html[yegor] started to store some substitutions in maps_Mon Sep 19 07:38:15 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-15-567671000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-15-567671000-PDT.html[yegor] almost all substitutions are now maps_Mon Sep 19 07:38:16 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-16-188243000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-16-188243000-PDT.html[yegor] removed an unused function_Mon Sep 19 07:38:16 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-16-751334000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-16-751334000-PDT.html[jyh] Update to match the recent changes to omake._Mon Sep 19 07:38:17 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-17-257985000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-17-257985000-PDT.html[yegor] instead of collecting a sublist and then testing if its empty, return boolean as you go over theoriginal._Mon Sep 19 07:38:17 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-17-698391000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-17-698391000-PDT.html[] This commit was manufactured by cvs2svn to create branch _S4_jprover_._Mon Sep 19 07:38:18 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-18-246166000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-18-246166000-PDT.html[yegor] minor optimization_Mon Sep 19 07:38:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-33-973263000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-33-973263000-PDT.html[yegor] started to work on S4 part in jprover_Mon Sep 19 07:38:34 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-34-484588000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-34-484588000-PDT.html[yegor] added support for multi_conclusion sequents but there_s a lot of work for the other side of the interface_Mon Sep 19 07:38:35 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-35-253694000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-35-253694000-PDT.html[yegor] it finally compiles_Mon Sep 19 07:38:35 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-35-842545000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-35-842545000-PDT.html[yegor] Reformatting mainly_ there were several deeply nested if_s, I made flat indentation._Mon Sep 19 07:38:36 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-36-364035000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-36-364035000-PDT.html[yegor] the ways negation and implication are converted to tree nodes are different for intiotionistic and classical/s4 logics_Mon Sep 19 07:38:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-37-124274000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-37-124274000-PDT.html[yegor] cleaning other places that were tightly bound to J_Mon Sep 19 07:38:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-37-849635000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-37-849635000-PDT.html[yegor] Some time ago I unintentionally introduced a deviation from canonical algorithm_Mon Sep 19 07:38:38 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-38-454984000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-38-454984000-PDT.html[yegor] more S4_related modifications_Mon Sep 19 07:38:38 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-38-970826000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-38-970826000-PDT.html[yegor] same predicate was computed on every iteration, moved it outside_Mon Sep 19 07:38:39 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-39-559440000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-39-559440000-PDT.html[yegor] moved computation of another predicate outside of recursive function_Mon Sep 19 07:38:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-40-110609000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-40-110609000-PDT.html[yegor] Gentzen style S4 and its connection with Jprover_Mon Sep 19 07:38:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-40-665716000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-40-665716000-PDT.html[yegor] my S4 does not have so I simplified its interface with Jprover_Mon Sep 19 07:38:41 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-41-330947000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-41-330947000-PDT.html[yegor] We have at least partly working S4_prover. It can prove reflexivity, transitivity,_Mon Sep 19 07:38:41 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-41-750595000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-41-750595000-PDT.html[yegor] 1. assumptions were incorrectly ordering in and_intro, fixed._Mon Sep 19 07:38:45 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-45-450860000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-45-450860000-PDT.html[yegor] forgot .cvsignore_Mon Sep 19 07:38:50 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-50-453693000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-50-453693000-PDT.html[yegor] Merging S4_prover to the main trunk_Mon Sep 19 07:38:50 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-50-813798000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-50-813798000-PDT.html[nogin] Added Nuprl_font_tensor_ more dforms for Nuprl_font_circ._Mon Sep 19 07:38:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-55-655727000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-55-655727000-PDT.html[nogin] If Jprover generates a subgoal with a conclusion that is identical to the_Mon Sep 19 07:38:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-56-104631000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-56-104631000-PDT.html[nogin] ____ WARNING_ breaks binary compatibility_ _____Mon Sep 19 07:38:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-56-518461000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-56-518461000-PDT.html[yegor] removed the last place where string encoding was used_Mon Sep 19 07:38:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-56-979159000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-56-979159000-PDT.html[yegor] Forcing JProver to use atoms from conclusion first._Mon Sep 19 07:38:57 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-57-524045000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-57-524045000-PDT.html[nogin] This is a huge commit that is mostly no_op__Mon Sep 19 07:38:58 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-58-074951000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-38-58-074951000-PDT.html[nogin] More preamble changes_Mon Sep 19 07:39:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-30-253370000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-30-253370000-PDT.html[yegor] Probably a non_working draft of lifting lemma and deduction theorem procedures_Mon Sep 19 07:39:31 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-31-444702000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-31-444702000-PDT.html[nogin] Added symbols_ box, bigcirc._Mon Sep 19 07:39:31 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-31-937161000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-31-937161000-PDT.html[nogin] Added Mpsymbols_multimap_Mon Sep 19 07:39:32 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-32-363930000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-32-363930000-PDT.html[nogin] Adding a preminimary implementation of the ILC basics in MetaPRL_Mon Sep 19 07:39:32 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-32-779794000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-32-779794000-PDT.html[nogin] Minor display forms update_Mon Sep 19 07:39:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-33-710669000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-33-710669000-PDT.html[jyh] Convert to using normal conditionals for metaprl.tex to get it to work_Mon Sep 19 07:39:34 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-34-188019000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-34-188019000-PDT.html[yegor] Added an example that shows that LP_multiplicity has no counterpart in S4._Mon Sep 19 07:39:38 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-38-394970000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-38-394970000-PDT.html[yegor] Groundwork for multi_modal S4._Mon Sep 19 07:39:52 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-52-396545000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-52-396545000-PDT.html[yegor] Yesterday I added two new position kinds indexed by integers to support multiple modalities._Mon Sep 19 07:39:53 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-53-450746000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-53-450746000-PDT.html[yegor] Better error messages when trying to turn something weird into a variable._Mon Sep 19 07:39:54 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-54-181497000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-54-181497000-PDT.html[yegor] S4 is working again._Mon Sep 19 07:39:54 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-54-605332000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-39-54-605332000-PDT.html[yegor] Some minor fixes._Mon Sep 19 07:40:18 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-18-963496000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-18-963496000-PDT.html[yegor] Apparently the prefix unification algorithm is incorrect,_Mon Sep 19 07:40:19 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-19-550359000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-19-550359000-PDT.html[yegor] Now I have problem with recosntruction of the correct ordering of inferences._Mon Sep 19 07:40:19 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-19-997751000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-19-997751000-PDT.html[nogin] Committing Limin_s current version of the ILC theory _with a few minor_Mon Sep 19 07:40:21 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-21-018678000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-21-018678000-PDT.html[nogin] Updating CVS instructions with the latest information._Mon Sep 19 07:40:21 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-21-565598000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-21-565598000-PDT.html[yegor] Some fixes in the unification algorithm _ it is _still_ too agressive in_Mon Sep 19 07:40:21 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-21-998196000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-21-998196000-PDT.html[nogin] _ Added the impl_intro to the intro resource_Mon Sep 19 07:40:22 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-22-484470000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-22-484470000-PDT.html[yegor] a little _better_ unification_Mon Sep 19 07:40:22 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-22-880981000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-22-880981000-PDT.html[nogin] Do not atempt to use ITT_JProver on non_ITT sequents._Mon Sep 19 07:40:23 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-23-311933000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-23-311933000-PDT.html[yegor] To make life easier added integer index to NewVarQ as well_Mon Sep 19 07:40:23 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-23-794220000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-23-794220000-PDT.html[yegor] added 2 more tests_Mon Sep 19 07:40:24 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-24-457217000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-24-457217000-PDT.html[yegor] simplified multimodal compatibility conditions_Mon Sep 19 07:40:24 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-24-842982000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-24-842982000-PDT.html[nogin] Minor code simplification_Mon Sep 19 07:40:25 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-25-342704000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-25-342704000-PDT.html[nogin] A few more minor code simplifications_Mon Sep 19 07:40:25 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-25-866986000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-25-866986000-PDT.html[nogin] Use opname instead of operator as a _predicate_ identifier in JProver. Opname_Mon Sep 19 07:40:26 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-26-437592000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-26-437592000-PDT.html[nogin] Getting rid of the _multiple ways to build scanner _scanner_Mon Sep 19 07:40:27 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-27-032158000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-27-032158000-PDT.html[nogin] Implemented _omake FORCE_REALCLEAN_1 realclean_ allowing for a forced_Mon Sep 19 07:40:27 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-27-447837000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-27-447837000-PDT.html[yegor] A pair of an item and a list was returned as a list, changed it to a real pair._Mon Sep 19 07:40:27 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-27-843955000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-27-843955000-PDT.html[yegor] more tests_Mon Sep 19 07:40:28 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-28-408834000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-28-408834000-PDT.html[yegor] from now on positions are compared by their indices only_Mon Sep 19 07:40:29 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-29-658610000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-29-658610000-PDT.html[yegor] replaced several __comparisons of positions with defined comparison_Mon Sep 19 07:40:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-30-053888000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-30-053888000-PDT.html[nogin] Added an ad_hoc profiling mechanism._Mon Sep 19 07:40:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-30-607693000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-30-607693000-PDT.html[nogin] Setenv MP_DEBUG earier to make sure all the .SUBDIRS directives are in scope._Mon Sep 19 07:40:31 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-31-055262000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-31-055262000-PDT.html[yegor] two more ___ replaced with position_eq_Mon Sep 19 07:40:31 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-31-451372000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-31-451372000-PDT.html[yegor] more ___ replaced with position_eq_Mon Sep 19 07:40:31 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-31-963851000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-31-963851000-PDT.html[nogin] When the same debug flag is created several times, make sure debug_description_Mon Sep 19 07:40:32 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-32-509876000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-32-509876000-PDT.html[nogin] Added code for ad_hoc profiling of top_level tactics. The profiling is_Mon Sep 19 07:40:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-33-091199000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-33-091199000-PDT.html[yegor] more position_eq instead of _, one place needs _ because index 0 is not globally unique_Mon Sep 19 07:40:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-33-827114000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-33-827114000-PDT.html[nogin] The record_reduceT tactic had rwh on top of higherC, fixing._Mon Sep 19 07:40:34 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-34-388794000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-34-388794000-PDT.html[nogin] Added rewrite profiling to tactic_profile._Mon Sep 19 07:40:34 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-34-810753000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-34-810753000-PDT.html[nogin] Minor optimization._Mon Sep 19 07:40:36 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-36-184558000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-36-184558000-PDT.html[yegor] one more test_Mon Sep 19 07:40:36 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-36-565352000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-36-565352000-PDT.html[yegor] replaced generic jprover_bug exception with more specific ones refering to a particular function where a problem happened_Mon Sep 19 07:40:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-37-608198000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-37-608198000-PDT.html[yegor] finally it is smart enough to apply rules in the right order while proving_Mon Sep 19 07:40:38 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-38-276938000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-38-276938000-PDT.html[yegor] ___ Wise men puzzle proved ____Mon Sep 19 07:40:39 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-39-092194000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-39-092194000-PDT.html[yegor] muddy children are also partially working but the problem here seems to be in performance_Mon Sep 19 07:40:39 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-39-545419000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-39-545419000-PDT.html[yegor] forgot to remove a couple of debug messages_Mon Sep 19 07:40:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-40-378593000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-40-378593000-PDT.html[yegor] 2 and 3 muddy children problems are solved._Mon Sep 19 07:40:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-40-893301000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-40-893301000-PDT.html[yegor] I changed a theorem statement and its proof became _infinite_, this commit removes the proof._Mon Sep 19 07:40:42 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-42-518388000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-42-518388000-PDT.html[yegor] replaced a list with a map_Mon Sep 19 07:40:43 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-43-868953000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-43-868953000-PDT.html[yegor] removed an unused parameter in a group of functions_Mon Sep 19 07:40:44 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-44-411116000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-44-411116000-PDT.html[yegor] replaced a custom function with Set.filter_Mon Sep 19 07:40:44 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-44-977026000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-44-977026000-PDT.html[yegor] several renamings and one custom functions replaced with List.fold_left_Mon Sep 19 07:40:45 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-45-554226000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-45-554226000-PDT.html[yegor] more on conversion lists to maps_Mon Sep 19 07:40:46 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-46-098256000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-46-098256000-PDT.html[yegor] more list converted to maps_Mon Sep 19 07:40:47 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-47-765558000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-47-765558000-PDT.html[yegor] replaced a couple of ___ with position_eq and made one function tail_recursive_Mon Sep 19 07:40:50 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-50-418072000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-50-418072000-PDT.html[yegor] Until now, before calling unify_mm jprover used to apply previously found_Mon Sep 19 07:40:52 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-52-660770000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-52-660770000-PDT.html[yegor] Jprover used to replace original free variables with ground terms_Mon Sep 19 07:40:53 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-53-340427000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-53-340427000-PDT.html[yegor] Use Lm_symbol.new_number for unique indices instead of local counter._Mon Sep 19 07:40:53 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-53-968526000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-53-968526000-PDT.html[yegor] Second and the last local counter replaced with Lm_symbol.new_number_Mon Sep 19 07:40:54 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-54-766111000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-54-766111000-PDT.html[yegor] There is one more counter for unique indices, with this commit it is localized_Mon Sep 19 07:40:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-55-324657000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-55-324657000-PDT.html[yegor] 1.Made one exception more verbose_Mon Sep 19 07:40:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-55-994424000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-55-994424000-PDT.html[yegor] Until now Jprover used to replace all originally free variables with ground terms_Mon Sep 19 07:40:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-56-439148000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-56-439148000-PDT.html[yegor] Fixing a typo_Mon Sep 19 07:40:57 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-57-433464000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-57-433464000-PDT.html[yegor] turned a group of functions into tail_recursive form_Mon Sep 19 07:40:57 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-57-870062000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-57-870062000-PDT.html[yegor] a bunch of minor optimizations_Mon Sep 19 07:40:58 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-58-412430000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-58-412430000-PDT.html[yegor] replaced a couple of ___ with position_eq_Mon Sep 19 07:40:58 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-58-989537000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-58-989537000-PDT.html[jyh] Totally revising the file chapter._Mon Sep 19 07:40:59 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-59-538395000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-40-59-538395000-PDT.html[] This commit was manufactured by cvs2svn to create branch_Mon Sep 19 07:41:00 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-00-318422000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-00-318422000-PDT.html[yegor] I started to work on rule_based prefix unification in jprover._Mon Sep 19 07:41:16 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-16-336512000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-16-336512000-PDT.html[yegor] Made the rules_ map more intelligent _ after a rule found applicable use a predefined_Mon Sep 19 07:41:16 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-16-958965000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-16-958965000-PDT.html[yegor] a slight tune up_Mon Sep 19 07:41:17 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-17-423117000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-17-423117000-PDT.html[yegor] one rule was not applicable after another, so I removed it._Mon Sep 19 07:41:17 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-17-834173000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-17-834173000-PDT.html[yegor] minor optimizations_Mon Sep 19 07:41:18 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-18-245097000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-18-245097000-PDT.html[yegor] I don_t understand why rev_append worked in this place, rolling back to append_Mon Sep 19 07:41:18 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-18-820814000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-18-820814000-PDT.html[jyh] Modified the chapter on files._Mon Sep 19 07:41:19 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-19-243631000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-19-243631000-PDT.html[yegor] preparations for continuation support_Mon Sep 19 07:41:20 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-20-559840000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-20-559840000-PDT.html[yegor] The infrastructure for continuation in prefix unification is ready._Mon Sep 19 07:41:21 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-21-040440000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-21-040440000-PDT.html[yegor] Replaced an append with rev_append_Mon Sep 19 07:41:21 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-21-614641000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-21-614641000-PDT.html[yegor] another ___ replaced with position_eq_Mon Sep 19 07:41:22 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-22-035313000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-22-035313000-PDT.html[yegor] It_s amazing, continuation worked well from the first try without any debugging__Mon Sep 19 07:41:22 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-22-445574000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-22-445574000-PDT.html[yegor] Merging continuation code into the main trunk_Mon Sep 19 07:41:23 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-23-200721000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-23-200721000-PDT.html[yegor] With the new unification algorithm muddy children problem for 4 children_Mon Sep 19 07:41:24 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-24-181085000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-24-181085000-PDT.html[yegor] S4_to_LP realization compiles but definitely does not work yet._Mon Sep 19 07:41:24 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-24-734134000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-24-734134000-PDT.html[yegor] Sounds funny, but I missed the stage when non_essential boxes are actually converted to proof terms._Mon Sep 19 07:41:25 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-25-578059000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-25-578059000-PDT.html[yegor] Now box should be timely converted to proof terms, it_s time to see how the whole thing works._Mon Sep 19 07:41:26 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-26-040893000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-26-040893000-PDT.html[yegor] Now it seems to be capable of realizing S4 proof of box_a __ a_ in LP._Mon Sep 19 07:41:26 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-26-512746000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-26-512746000-PDT.html[yegor] Forgot to remove debug messages._Mon Sep 19 07:41:27 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-27-071522000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-07/2005-09-19-07-41-27-071522000-PDT.html