[yegor] My first two proofs_int_sqequal_rw and beq_int_is_true_rw__ Mon Sep 19 02:47:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-44-547787000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-44-547787000-PDT.html [yegor] finishSq2ExT_ term__int__tactic added._ Mon Sep 19 02:47:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-48-333167000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-48-333167000-PDT.html [yegor] missprint in uni_add_Distrib is fixed_ Mon Sep 19 02:47:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-48-730276000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-48-730276000-PDT.html [yegor] add_Id2C added it is a commutative pair of add_IdC_ Mon Sep 19 02:47:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-49-138194000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-49-138194000-PDT.html [yegor] Most interactives are proved. Only most difficult to me remain_ Mon Sep 19 02:47:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-49-518036000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-49-518036000-PDT.html [kopylov] Now the letT tactic takes a term x_s in S as an argument _instead of s in S_._ Mon Sep 19 02:47:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-58-023824000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-58-023824000-PDT.html [krupski] ___ empty log message ____ Mon Sep 19 02:47:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-58-401374000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-58-401374000-PDT.html [yegor] sqeq2rwT_ tactic __ tactic added. It apply argument and then make all conversions from squash to ext. It is useful to proving rewrites derived from sqequal_rules_ Mon Sep 19 02:47:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-58-903507000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-58-903507000-PDT.html [yegor] All rewrites derived from sq_rules are proved with sqeq2rwT now._ Mon Sep 19 02:47:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-59-305087000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-47-59-305087000-PDT.html [nogin] Make foldC work on conditional rewrites._ Mon Sep 19 02:48:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-03-841171000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-03-841171000-PDT.html [nogin] I_ve added a cvsweb script that I believe to be quite useful._ Mon Sep 19 02:48:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-06-937555000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-06-937555000-PDT.html [kopylov] The itt_squiggle theory is added at last._ Mon Sep 19 02:48:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-07-347335000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-07-347335000-PDT.html [kopylov] The build term is moved from Itt_struct to Itt_equal._ Mon Sep 19 02:48:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-08-983760000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-08-983760000-PDT.html [nogin] I moved the bind operator from ITT to the Perv module. This makes sense because_ Mon Sep 19 02:48:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-09-587233000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-09-587233000-PDT.html [kopylov] _ Mon Sep 19 02:48:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-17-706758000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-17-706758000-PDT.html [kopylov] I return the name Perv_rewrite for _. So one can use both mechanisms for applying conditional rewrites__ Mon Sep 19 02:48:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-19-399487000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-19-399487000-PDT.html [nogin] Removed some duplicated printing code._ Mon Sep 19 02:48:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-19-827152000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-19-827152000-PDT.html [nogin] I wrote a small hack that should check free variables in conditional rewrite_ Mon Sep 19 02:48:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-21-339248000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-21-339248000-PDT.html [krupski] _ Mon Sep 19 02:48:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-21-948483000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-21-948483000-PDT.html [yegor] Most of rules are proved. Elimination rule fixed and proved._ Mon Sep 19 02:48:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-24-383466000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-24-383466000-PDT.html [nogin] Link to OpenSSH home page._ Mon Sep 19 02:48:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-27-847040000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-27-847040000-PDT.html [krupski] ._ Mon Sep 19 02:48:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-28-203433000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-28-203433000-PDT.html [krupski] for Rob_ds testing_ Mon Sep 19 02:48:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-29-700289000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-29-700289000-PDT.html [krupski] Rob_ds functions added _for testing only_._ Mon Sep 19 02:48:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-30-086290000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-30-086290000-PDT.html [yegor] 1.Display forms taken from old itt_int_ Mon Sep 19 02:48:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-30-541478000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-30-541478000-PDT.html [nogin] Updated the CVS doc link._ Mon Sep 19 02:48:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-34-956305000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-34-956305000-PDT.html [yegor] All interactive rules are proved_ Mon Sep 19 02:48:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-36-373290000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-36-373290000-PDT.html [nogin] TODO_ Better matching in dT_ Mon Sep 19 02:48:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-55-402750000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-55-402750000-PDT.html [nogin] _ Fixed a nasty bug in indEquality. Yegor, can you dbl_check, please__ Mon Sep 19 02:48:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-55-761072000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-02/2005-09-19-02-48-55-761072000-PDT.html