[jyh] Addec cs136._Wed Feb 1 11:51:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-01-11-51-30-132964000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-01-11-51-30-132964000-PST.html[xiny] Defined BTerms as the basic terms, instead of defining it based on languages._Thu Feb 2 14:57:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-02-14-57-31-120113000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-02-14-57-31-120113000-PST.html[jyh] Preparing to move _append sequents_ to obsolete status._Sun Feb 5 11:36:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-05-11-36-03-274487000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-05-11-36-03-274487000-PST.html[jyh] Moved append/flat sequents into theories/itt/reflection/obsolete_flat_Sun Feb 5 11:54:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-05-11-54-19-866970000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-05-11-54-19-866970000-PST.html[nogin] Itt_bool does not depend on Itt_set._Mon Feb 6 17:14:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-06-17-14-13-173592000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-06-17-14-13-173592000-PST.html[nogin] Minor optimization._Mon Feb 6 23:20:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-06-23-20-25-644095000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-06-23-20-25-644095000-PST.html[nogin] Minor cleanup._Tue Feb 7 00:00:51 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-00-00-51-304631000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-00-00-51-304631000-PST.html[nogin] Made the script a bit more flexible._Tue Feb 7 18:31:00 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-18-31-00-776520000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-18-31-00-776520000-PST.html[nogin] Alexei _ Aleksey__Tue Feb 7 19:25:55 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-19-25-55-909178000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-19-25-55-909178000-PST.html[nogin] Alexei _ Aleksey__Tue Feb 7 21:23:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-21-23-38-804955000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-07-21-23-38-804955000-PST.html[nogin] _ Fixed a rewriter bug uncovered by a recent change to let_rule rule._Wed Feb 8 00:56:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-00-56-24-266833000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-00-56-24-266833000-PST.html[nogin] ___ Warning_ breaks binary compatibility_ ____Wed Feb 8 02:05:49 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-02-05-49-171422000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-02-05-49-171422000-PST.html[nogin] Removing an outdated comment._Wed Feb 8 14:58:36 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-14-58-36-908331000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-14-58-36-908331000-PST.html[nogin] _ Changed the filter to add a _Perv_select_crw_ label to all the annotations_Wed Feb 8 20:20:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-20-20-52-526484000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-20-20-52-526484000-PST.html[nogin] Minor variable naming fix._Wed Feb 8 20:54:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-20-54-02-304557000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-20-54-02-304557000-PST.html[nogin] Small simplification of definitions._Wed Feb 8 23:05:18 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-23-05-18-967773000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-08-23-05-18-967773000-PST.html[nogin] Minor improvements in reduce resource for the number theory_Thu Feb 9 02:35:00 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-02-35-00-345032000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-02-35-00-345032000-PST.html[nogin] The way we had __ and __ defined with reduceT _randomly_ turning __ into ___Thu Feb 9 14:32:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-14-32-20-266184000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-14-32-20-266184000-PST.html[nogin] Fixed a proof broken by the previous commit._Thu Feb 9 14:36:50 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-14-36-50-340095000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-14-36-50-340095000-PST.html[nogin] Proven much stronger elimination rules for Image and union types._Thu Feb 9 21:32:49 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-21-32-49-579047000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-21-32-49-579047000-PST.html[nogin] _ Implemented the splitNatT tactic that does case wplit _0 or not_ for a_Thu Feb 9 23:16:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-23-16-13-036336000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-09-23-16-13-036336000-PST.html[nogin] Derived the itt_list theory__Fri Feb 10 00:44:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-00-44-19-536248000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-00-44-19-536248000-PST.html[nogin] Turns out that we do not really need the _weak reverse functionality_ axiom_Fri Feb 10 01:04:28 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-01-04-28-554714000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-01-04-28-554714000-PST.html[yegor] Added a missing comma in addsuffix, relevant to win32 only_Fri Feb 10 12:06:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-12-06-23-907792000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-12-06-23-907792000-PST.html[yegor] Tiny typo_Fri Feb 10 12:10:12 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-12-10-12-146420000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-10-12-10-12-146420000-PST.html[jyh] Working on .cmoz conversion._Sun Feb 12 18:20:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-18-20-46-416918000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-18-20-46-416918000-PST.html[jyh] Fixed filter_bin__its been broken for a long time._Sun Feb 12 18:59:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-18-59-24-324942000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-18-59-24-324942000-PST.html[jyh] Might as well fix the _convert_ program too._Sun Feb 12 19:15:44 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-19-15-44-130416000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-19-15-44-130416000-PST.html[nogin] Reverted revisions 8657, 8659, and 8660. These revisions have made the_Sun Feb 12 20:13:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-20-13-37-857628000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-20-13-37-857628000-PST.html[nogin] Weakened the nilEquality axiom, replacing the_Sun Feb 12 21:06:26 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-21-06-26-970143000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-21-06-26-970143000-PST.html[nogin] Boolean rules should be producing asserts instead of boolean equalities._Sun Feb 12 22:41:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-22-41-02-114624000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-22-41-02-114624000-PST.html[nogin] Maked a conditional rewrite in reduce resource._Sun Feb 12 23:32:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-23-32-03-904157000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-12-23-32-03-904157000-PST.html[nogin] Using Itt_pairwise, proved stronger elimination rules for the image type _for_Mon Feb 13 01:02:26 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-01-02-26-340240000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-01-02-26-340240000-PST.html[nogin] Derived itt_list from itt_union _ itt_nat__Mon Feb 13 02:07:00 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-07-00-590938000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-07-00-590938000-PST.html[nogin] _Strong_ elimination rules _dprod, prod, disjoint union_ should be formulated_Mon Feb 13 02:44:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-44-19-751652000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-44-19-751652000-PST.html[nogin] Getting rid of gt and gt_bool operators _ turning them into iforms for lt and_Mon Feb 13 02:46:08 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-46-08-156873000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-46-08-156873000-PST.html[nogin] Filled in the proofs _do we actually need this module___Mon Feb 13 02:49:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-49-23-344245000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-02-49-23-344245000-PST.html[nogin] Annotated some manual adds to reduce as conditional rewrites._Mon Feb 13 12:58:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-12-58-17-887101000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-12-58-17-887101000-PST.html[nogin] Getting rid of the Itt_hoas_lang theory _moving it to obsolete_, deriving the_Mon Feb 13 15:37:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-15-37-23-686428000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-15-37-23-686428000-PST.html[nogin] The previos commit broke a few proofs, fixing._Mon Feb 13 16:57:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-16-57-53-330549000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-16-57-53-330549000-PST.html[nogin] Adding reduce_vsubst_dummy_null to reduce._Mon Feb 13 17:43:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-17-43-10-478070000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-17-43-10-478070000-PST.html[nogin] Simplified the Itt_vec_sequent_term theory a bit._Mon Feb 13 19:17:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-19-17-02-323078000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-19-17-02-323078000-PST.html[nogin] Another small simplification _trying to make sure that rewrites do not have_Mon Feb 13 21:19:32 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-21-19-32-984710000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-21-19-32-984710000-PST.html[nogin] _ Removing a duplicate rule_ Itt_vec_sequent_term.reduce_nth_of_list_of_fun was_Mon Feb 13 21:45:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-21-45-54-948806000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-21-45-54-948806000-PST.html[nogin] Adding hyps_length_null to reduce_Mon Feb 13 22:06:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-22-06-34-922486000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-22-06-34-922486000-PST.html[nogin] Swapped reduce_hyps_flatten_bind_nil1 and reduce_hyps_flatten_bind_nil2_Mon Feb 13 22:29:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-22-29-47-959575000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-13-22-29-47-959575000-PST.html[nogin] _ Added nth_hyp annotations to _lots_ of rules _especially in the algerba_Tue Feb 14 02:20:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-02-20-54-295973000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-02-20-54-295973000-PST.html[nogin] Removed Itt_hoas_lang from the list of the printed theories._Tue Feb 14 13:31:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-13-31-10-380193000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-13-31-10-380193000-PST.html[nogin] Slightly more efficient nthHypT and Itt_struct.nthAssumT_Tue Feb 14 13:31:48 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-13-31-48-041095000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-13-31-48-041095000-PST.html[nogin] Term_match_table_ use options instead if Not_found exceptions to communicate_Tue Feb 14 15:13:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-15-13-24-617839000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-15-13-24-617839000-PST.html[nogin] Removing a duplicate rule._Tue Feb 14 16:03:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-16-03-53-839851000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-16-03-53-839851000-PST.html[nogin] Minor intro resource annotation change_Tue Feb 14 18:11:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-18-11-40-904112000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-18-11-40-904112000-PST.html[jyh] Added the template for reflecting theories from the .cmoz file._Tue Feb 14 18:49:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-18-49-27-473439000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-18-49-27-473439000-PST.html[nogin] Small resource update._Tue Feb 14 19:04:06 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-19-04-06-928374000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-19-04-06-928374000-PST.html[jyh] Doh,_Tue Feb 14 19:17:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-19-17-10-554263000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-19-17-10-554263000-PST.html[nogin] Adding a temporary hack to account for the fact that reflected theories have_Tue Feb 14 19:55:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-19-55-30-254875000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-19-55-30-254875000-PST.html[nogin] MLZFILES should be symlinked before scanning for dependencies._Tue Feb 14 20:32:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-20-32-59-808221000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-20-32-59-808221000-PST.html[nogin] All the reflected theories depend on itt_hoas_theory._Tue Feb 14 21:46:36 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-21-46-36-923099000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-21-46-36-923099000-PST.html[nogin] _ Filter_reflection_ module names should not be capitalized._Tue Feb 14 22:59:21 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-22-59-21-515285000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-14-22-59-21-515285000-PST.html[nogin] Fixing a typo._Wed Feb 15 00:23:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-00-23-40-672166000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-00-23-40-672166000-PST.html[nogin] Making the nth_hyp resource a bit more precise._Wed Feb 15 01:01:50 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-01-01-50-091289000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-01-01-50-091289000-PST.html[nogin] Adding conjunction elimination to the nth_hyp resource._Wed Feb 15 02:01:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-02-01-31-658944000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-02-01-31-658944000-PST.html[nogin] Making the nth_hyp annotation processor slightly more precise_Wed Feb 15 03:25:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-03-25-52-964960000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-03-25-52-964960000-PST.html[nogin] Exposing the _in_auto_ function in the interface._Wed Feb 15 05:16:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-05-16-29-667415000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-05-16-29-667415000-PST.html[nogin] Added a few nth_hyp annotations_Wed Feb 15 06:26:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-06-26-53-128835000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-06-26-53-128835000-PST.html[nogin] We do not need this OMakefile _it duplicates a part of the code that I_ve_Wed Feb 15 12:48:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-12-48-46-449597000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-12-48-46-449597000-PST.html[nogin] Keep the pnm_core_logic in the default build for now._Wed Feb 15 13:38:55 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-13-38-55-428881000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-13-38-55-428881000-PST.html[nogin] Adding squash_compatible_shapes_...__ to the elim resource._Wed Feb 15 16:34:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-16-34-31-005475000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-16-34-31-005475000-PST.html[nogin] Better usage of bySubtypeT._Wed Feb 15 18:37:22 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-18-37-22-867869000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-18-37-22-867869000-PST.html[nogin] Negation is squash_stable _when well_typed_._Wed Feb 15 21:54:21 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-21-54-21-285352000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-21-54-21-285352000-PST.html[nogin] _ Added an AutoOK option to elim rule annotations. The rules marked with_Wed Feb 15 23:04:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-23-04-23-050677000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-15-23-04-23-050677000-PST.html[nogin] Negation is squash_stable _when well_typed_._Thu Feb 16 02:18:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-02-18-04-249257000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-02-18-04-249257000-PST.html[nogin] _ Added an AutoOK option to elim rule annotations. The rules marked with_Thu Feb 16 02:18:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-02-18-04-249863000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-02-18-04-249863000-PST.html[nogin] Now that _ and __ are iforms, we should not have a separate omegaT entries for_Thu Feb 16 17:14:26 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-17-14-26-086070000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-17-14-26-086070000-PST.html[jyh] Temporarily removed Aleksey_s reflection dependency code._Thu Feb 16 18:12:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-18-12-13-477659000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-16-18-12-13-477659000-PST.html[nogin] Symlinks for .mlz should not a part of the repository._Fri Feb 17 01:31:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-01-31-54-292519000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-01-31-54-292519000-PST.html[jyh] Working on dependencies and despagettification of ocamldep._Fri Feb 17 12:16:48 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-12-16-48-158056000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-12-16-48-158056000-PST.html[nogin] Ignore the reflect_base_theory._ml,mli_ symlinks._Fri Feb 17 12:18:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-12-18-10-401073000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-12-18-10-401073000-PST.html[nogin] Fixing a typo._Fri Feb 17 12:45:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-12-45-53-716625000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-12-45-53-716625000-PST.html[kopylov] Defined set and squash types using image type._Fri Feb 17 15:18:36 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-15-18-36-933357000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-15-18-36-933357000-PST.html[nogin] Now that the squash is a defined operator and not a postulated one, I am a bit_Fri Feb 17 15:47:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-15-47-59-956355000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-15-47-59-956355000-PST.html[nogin] The squash resource should not rely on dT 0._Fri Feb 17 16:07:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-16-07-15-333833000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-16-07-15-333833000-PST.html[nogin] Reducing constant inequalities in intro and elim was implemented a bit badly. For_Fri Feb 17 17:49:51 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-17-49-51-180048000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-17-49-51-180048000-PST.html[kopylov] 1. Added a new tactic_Fri Feb 17 18:08:50 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-18-08-50-625147000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-18-08-50-625147000-PST.html[nogin] Added _ _a__b in nat ___ _a in int _ and _ _a__b in nat ___ _b in int _ to_Fri Feb 17 18:29:07 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-18-29-07-884019000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-17-18-29-07-884019000-PST.html[nogin] Removing a redundant rule _should have been removed when gt became an iform_Sat Feb 18 20:12:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-18-20-12-13-724604000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-18-20-12-13-724604000-PST.html[nogin] Adding _ n in nat __ n __ 0_ to the nth_hyp resource._Sat Feb 18 20:24:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-18-20-24-02-176568000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-18-20-24-02-176568000-PST.html[jyh] Finished despaghettification of ocamldep.mll._Sun Feb 19 13:27:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-13-27-34-737492000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-13-27-34-737492000-PST.html[nogin] Use simpleReduceT instead of _rw reduceC 0_ before omegaT in intro._Sun Feb 19 16:12:42 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-16-12-42-522016000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-16-12-42-522016000-PST.html[jyh] Added reflection conversion for term declarations._Sun Feb 19 16:58:50 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-16-58-50-349441000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-16-58-50-349441000-PST.html[jyh] Add the other reflected theorems, including the elimination rule._Sun Feb 19 18:58:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-18-58-19-219940000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-18-58-19-219940000-PST.html[jyh] Boo, I have no idea why the dependencies for reflected files_Sun Feb 19 20:30:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-20-30-27-770323000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-20-30-27-770323000-PST.html[nogin] A few nth_hyp annotations in reflected theories._Sun Feb 19 23:00:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-23-00-25-138756000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-19-23-00-25-138756000-PST.html[jyh] Doh, the dependency problem was because OCaml uses the filename to_Mon Feb 20 11:41:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-11-41-03-896619000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-11-41-03-896619000-PST.html[jyh] Minor cleanup. Remove ReflectC from mk/prlcomp._Mon Feb 20 11:49:43 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-11-49-43-585993000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-11-49-43-585993000-PST.html[jyh] Oops, it looks like target_is_buildable does not_Mon Feb 20 13:01:58 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-13-01-58-912704000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-13-01-58-912704000-PST.html[nogin] _ Changed bneq_int into an iform._Mon Feb 20 16:08:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-16-08-54-724346000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-16-08-54-724346000-PST.html[nogin] _ Added an elimination rule for the neq_int proposition._Mon Feb 20 18:44:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-18-44-34-767177000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-18-44-34-767177000-PST.html[jyh] Squash the .ml dependencies_Mon Feb 20 20:07:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-20-07-46-839113000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-20-07-46-839113000-PST.html[nogin] No_op API change _ added _wrap_elim_auto_ok_._Mon Feb 20 20:28:55 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-20-28-55-073732000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-20-28-55-073732000-PST.html[yegor] Added var_elim3 for special case, noticed by Aleksey Nogin_Mon Feb 20 21:26:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-21-26-27-172495000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-21-26-27-172495000-PST.html[xiny] I_ve been trying to prove a better elimination rule. I think provable_elim1_Mon Feb 20 21:40:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-21-40-20-701149000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-21-40-20-701149000-PST.html[nogin] For hypothesis of the form _x_ int_, _x_ nat_, _x_ BTerm_, etc, where _x_ does_Mon Feb 20 21:46:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-21-46-25-263383000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-21-46-25-263383000-PST.html[nogin] Increasing the priority of a few elim resource entries_Mon Feb 20 22:13:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-22-13-24-195006000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-22-13-24-195006000-PST.html[nogin] Expose d_elim_prec._Mon Feb 20 22:28:48 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-22-28-48-668206000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-22-28-48-668206000-PST.html[nogin] Proved the Itt_hoas_proof_ind.provable_elim1. I_ve used pairwise functionality_Mon Feb 20 23:02:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-23-02-41-793896000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-20-23-02-41-793896000-PST.html[nogin] The unit elimination rule should thin._Tue Feb 21 00:12:28 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-00-12-28-807153000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-00-12-28-807153000-PST.html[nogin] Added _ a _ b in nat ___ b _ a in int _ to the nth_hyp resource._Tue Feb 21 00:36:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-00-36-04-875339000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-00-36-04-875339000-PST.html[nogin] Small optimization _a follow_up to my previous commit_._Tue Feb 21 00:55:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-00-55-59-684855000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-00-55-59-684855000-PST.html[nogin] Thin out useless BTerm__i_, BSequentCore and BSequentCore__i_ hypotheses._Tue Feb 21 01:12:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-01-12-10-307454000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-01-12-10-307454000-PST.html[nogin] Another nth_hyp improvement._Tue Feb 21 01:41:57 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-01-41-57-625192000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-01-41-57-625192000-PST.html[jyh] The rule generation code should use second_order variables for the logic._Tue Feb 21 11:12:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-12-38-999919000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-12-38-999919000-PST.html[jyh] Intermediate commit while I rename the files._Tue Feb 21 11:25:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-25-24-022553000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-25-24-022553000-PST.html[jyh] Use new method of generating reflected theories._Tue Feb 21 11:32:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-32-17-269006000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-32-17-269006000-PST.html[nogin] This adds the simpleReduceT tactic to autoT on AutoNormal level._Tue Feb 21 11:45:48 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-45-48-504465000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-11-45-48-504465000-PST.html[jyh] For reflect_ theories, allow dependencies for reflect_theory.suffix_Tue Feb 21 14:22:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-14-22-46-129390000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-14-22-46-129390000-PST.html[jyh] Minor efficiency cleanup._Tue Feb 21 15:20:50 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-15-20-50-968890000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-15-20-50-968890000-PST.html[kopylov] 1. Defined singleton using the Image type._Tue Feb 21 19:09:51 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-19-09-51-843375000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-19-09-51-843375000-PST.html[kopylov] Fixed some source display forms_Tue Feb 21 19:45:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-19-45-25-744123000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-19-45-25-744123000-PST.html[kopylov] Updated some documentation_Tue Feb 21 19:54:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-19-54-19-707567000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-19-54-19-707567000-PST.html[jyh] This version, rather than having Reflect_foo extend Foo,_Tue Feb 21 20:05:07 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-20-05-07-302525000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-21-20-05-07-302525000-PST.html[nogin] Tiny progress towards the elimination tactic._Wed Feb 22 00:34:07 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-00-34-07-161891000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-00-34-07-161891000-PST.html[jyh] Simplify the elimination rule by omitting dependencies on the proof_Wed Feb 22 10:32:22 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-10-32-22-680565000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-10-32-22-680565000-PST.html[xiny] exists_list_elim shouldn_t have _i as one of the arguments._Wed Feb 22 15:36:18 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-15-36-18-808430000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-15-36-18-808430000-PST.html[kopylov] Fixed proofs broken by my last commit_Wed Feb 22 16:02:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-16-02-25-594934000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-16-02-25-594934000-PST.html[nogin] Minor improvements to rule statements generated by filter_reflection__Wed Feb 22 18:00:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-18-00-41-675542000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-18-00-41-675542000-PST.html[nogin] Adding the missing wf assumption to the elimination rule._Wed Feb 22 18:38:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-18-38-38-420378000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-18-38-38-420378000-PST.html[jyh] Removed the reflection code from Filter_parse._Wed Feb 22 18:48:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-18-48-24-382196000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-22-18-48-24-382196000-PST.html[nogin] Small proofRuleAuxWFT optimization,_Thu Feb 23 13:09:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-13-09-19-856520000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-13-09-19-856520000-PST.html[jyh] Copy display forms to reflected theories. The display forms_Thu Feb 23 19:01:28 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-19-01-28-691203000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-19-01-28-691203000-PST.html[jyh] Add display forms for judgments too._Thu Feb 23 19:05:58 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-19-05-58-146593000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-19-05-58-146593000-PST.html[jyh] Working on reflecting more stuff._Thu Feb 23 20:27:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-20-27-10-648817000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-23-20-27-10-648817000-PST.html[nogin] Added assert_bnot_a ___ b__ to the ge_elim resource._Fri Feb 24 15:54:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-24-15-54-40-739677000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-24-15-54-40-739677000-PST.html[nogin] Some helper lemmas for the elimination proof. Unfortunately the_Fri Feb 24 18:49:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-24-18-49-33-308886000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-24-18-49-33-308886000-PST.html[nogin] _ Allow nth_hyp annotations on forward_chaining rules that do not have wf_Sun Feb 26 12:22:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-26-12-22-52-302119000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-26-12-22-52-302119000-PST.html[nogin] _ Changed the definition of the SimpleStep predicate to include the wf_Sun Feb 26 12:56:35 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-26-12-56-35-945140000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-26-12-56-35-945140000-PST.html[yegor] The main subgoal of omegaT is completed by omegaT itself _it used to be deligated to autoT_._Mon Feb 27 13:54:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-13-54-38-915505000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-13-54-38-915505000-PST.html[nogin] Perv.bind should be polymorphic._Mon Feb 27 16:31:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-16-31-15-815890000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-16-31-15-815890000-PST.html[nogin] Removing a theorem that is not too useful._Mon Feb 27 18:23:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-18-23-11-326878000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-18-23-11-326878000-PST.html[nogin] Wrote a tactic that would apply hypC _or revHypC_ to the whole goal sequent,_Mon Feb 27 20:30:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-20-30-38-397990000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-20-30-38-397990000-PST.html[nogin] _ Defined a new suffic _ta_ that stands for _thenT autoT__Mon Feb 27 21:33:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-21-33-04-252773000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-27-21-33-04-252773000-PST.html[yegor] More flexible approach to proving the _main_ subgoal of omegaT_Tue Feb 28 08:12:55 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-08-12-55-348352000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-08-12-55-348352000-PST.html[yegor] forgot to commit auto_tactic.mli _ I need someNthHypT_Tue Feb 28 08:44:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-08-44-53-051494000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-08-44-53-051494000-PST.html[nogin] Partial reversal of Yegors_ recent changes to get omegaT to work again._Tue Feb 28 13:16:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-13-16-47-108558000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-13-16-47-108558000-PST.html[nogin] A few omegaT improvements based in part on Yegor_s recent changes._Tue Feb 28 14:40:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-14-40-17-774658000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-14-40-17-774658000-PST.html[nogin] Proactively run simpleReduceC on wf conditions generated by omegaT._Tue Feb 28 14:55:22 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-14-55-22-156018000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-14-55-22-156018000-PST.html[nogin] Added a wrap_intro_auto_complete helper function._Tue Feb 28 17:00:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-17-00-24-423317000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-17-00-24-423317000-PST.html[nogin] Minor optimization._Tue Feb 28 17:08:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-17-08-29-472469000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-17-08-29-472469000-PST.html[yegor] Removed an unused lemma._Tue Feb 28 20:22:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-20-22-03-647765000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-20-22-03-647765000-PST.html[nogin] The map_wf and map_wf4 rules have very strong wf conditions, so they need to_Tue Feb 28 23:24:55 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-23-24-55-124651000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-23-24-55-124651000-PST.html[nogin] Removed a large number of unnecessary wf conditions from Itt_list2 rules._Tue Feb 28 23:43:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-23-43-03-567259000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-02/2006-02-28-23-43-03-567259000-PST.html