Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-01 00:13:50 -0800 (Thu, 01 Feb 2001)
Revision: 3126
Log message:

      My first two proofs(int_sqequal_rw and beq_int_is_true_rw)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-01 03:33:12 -0800 (Thu, 01 Feb 2001)
Revision: 3127
Log message:

      finishSq2ExT: term->int->tactic added.
      It helps to complete prove of rewrites derived from ~-rules
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-01 05:27:23 -0800 (Thu, 01 Feb 2001)
Revision: 3128
Log message:

      missprint in uni_add_Distrib is fixed
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-01 06:04:24 -0800 (Thu, 01 Feb 2001)
Revision: 3129
Log message:

      add_Id2C added it is a commutative pair of add_IdC
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-01 06:08:15 -0800 (Thu, 01 Feb 2001)
Revision: 3130
Log message:

      Most interactives are proved. Only most difficult to me remain
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-01 11:22:00 -0800 (Thu, 01 Feb 2001)
Revision: 3131
Log message:

      Now the letT tactic takes a term x=s in S as an argument (instead of s in S).
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2001-02-01 15:19:13 -0800 (Thu, 01 Feb 2001)
Revision: 3132
Log message:

      *** empty log message ***
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-02 00:19:23 -0800 (Fri, 02 Feb 2001)
Revision: 3133
Log message:

      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
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-02 04:04:08 -0800 (Fri, 02 Feb 2001)
Revision: 3134
Log message:

      All rewrites derived from sq-rules are proved with sqeq2rwT now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-02 11:10:33 -0800 (Fri, 02 Feb 2001)
Revision: 3135
Log message:

      Make foldC work on conditional rewrites.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-02 15:04:39 -0800 (Fri, 02 Feb 2001)
Revision: 3136
Log message:

      I've added a cvsweb script that I believe to be quite useful.
      
      Usage: cvsweb [directory_or_file]
      
      The cvsweb script opens a new browser window showing the CVS entry for the specified
      file or directory. By default it shows the current directory.
      
      The script can be controlled by the following environment variables:
      CVSBASE - the base cvsweb URL. The default is http://cvs.cs.cornell.edu:12000/cvsweb/
      URLVIEW - the program to use to start the browser (the default is to use /usr/bin/netscape
                if it exists and "xterm -e lynx" otherwise)
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-02 15:16:21 -0800 (Fri, 02 Feb 2001)
Revision: 3137
Log message:

      The itt_squiggle theory is added at last.
      
      Now a ~ b is a type as well as any other type.
      To substitute 'a for 'b in nth clause you can use
      sqSubstT <<a ~ b>> n
      or you can use Itt_subst2.substT tactic instead. (Note that
      Itt_subst.substT  works only with an equality).
      
      The sqSubst tactic works exactly as the substT tactic.
      By default it replaces all occurrences of a with b, or
      one can give a bind term as an optional with-argument to specify
      the occurrences of a to be replaced.
      
      Example 1:
      
      H |- a+a=2*a
      by substT <<'a ~ 'b>> 0
      1.   ....rewrite....
           H |- a <--> b
      2.   ....main....
           H |- b+b=2*b
      
      Example 2:
      
      H |- a+a=2*a
      by withT <<bind{x.'x+'x=2*'a}>> (substT <<'a ~ 'b>> 0)
      1.   ....rewrite....
           H |- a <--> b
      2.   ....main....
           H |- b+b=2*a
      
      
      I'll document this theory later.
      
      Still to do: Figure out how to make conversion "a -> b" from "a~b".
      
      
      P.S. You probably need to run make clean in theories/itt before recompiling.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-03 17:18:47 -0800 (Sat, 03 Feb 2001)
Revision: 3138
Log message:

      The build term is moved from Itt_struct to Itt_equal.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-04 11:38:29 -0800 (Sun, 04 Feb 2001)
Revision: 3139
Log message:

      I moved the bind operator from ITT to the Perv module. This makes sense because
      what we really mean by "bind" is a generic binding construction, not something
      ITT-specific.
      I've also replaced Perv!lambda with Perv!bind since it was now redundant
      and it was indeed used as "bind", not as "lambda" (there were no beta-reduction
      for Perv!lambda).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-04 16:38:18 -0800 (Sun, 04 Feb 2001)
Revision: 3140
Log message:

      
      For now 'a~'b produces Itt_squiggle!sqeq{'a;'b} rather then Perv!rewrite.
      
      I documented the Itt_squiggle theory (see all-theories.pdf).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-05 12:00:52 -0800 (Mon, 05 Feb 2001)
Revision: 3141
Log message:

      I return the name Perv!rewrite for ~. So one can use both mechanisms for applying conditional rewrites:
      the old one and the new one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-05 13:14:58 -0800 (Mon, 05 Feb 2001)
Revision: 3142
Log message:

      Removed some duplicated printing code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-05 15:46:31 -0800 (Mon, 05 Feb 2001)
Revision: 3143
Log message:

      I wrote a small hack that should check free variables in conditional rewrite
      applications. This is a temporary measure (until we implement the correct
      mechanism for gereric rewriting), so I haven't spent too much time on making
      sure it will always work correctly.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2001-02-06 15:46:55 -0800 (Tue, 06 Feb 2001)
Revision: 3144
Log message:

      
      occurcheck implemented
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-07 01:06:43 -0800 (Wed, 07 Feb 2001)
Revision: 3145
Log message:

      Most of rules are proved. Elimination rule fixed and proved.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-11 17:37:21 -0800 (Sun, 11 Feb 2001)
Revision: 3147
Log message:

      Link to OpenSSH home page.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2001-02-14 13:16:28 -0800 (Wed, 14 Feb 2001)
Revision: 3148
Log message:

      .
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2001-02-14 13:27:58 -0800 (Wed, 14 Feb 2001)
Revision: 3149
Log message:

      for Rob_ds testing
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2001-02-14 13:36:28 -0800 (Wed, 14 Feb 2001)
Revision: 3150
Log message:

      Rob_ds functions added (for testing only).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-21 05:58:17 -0800 (Wed, 21 Feb 2001)
Revision: 3151
Log message:

      1.Display forms taken from old itt_int
      2.meta-evaluation on constants taken from old itt_int
      3.Some proofs added, "terrible" elim-rule fixed once again
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-22 11:21:57 -0800 (Thu, 22 Feb 2001)
Revision: 3153
Log message:

      Updated the CVS doc link.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-02-23 03:57:07 -0800 (Fri, 23 Feb 2001)
Revision: 3154
Log message:

      All interactive rules are proved
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-24 04:25:11 -0800 (Sat, 24 Feb 2001)
Revision: 3158
Log message:

      TODO: Better matching in dT
      make: added an .mlz file to the appropriate variable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-24 05:04:46 -0800 (Sat, 24 Feb 2001)
Revision: 3159
Log message:

      - Fixed a nasty bug in indEquality. Yegor, can you dbl-check, please?
      - Renamed "uni_minus" to "minus".
      - << (- 'a) >> is now parsed correctly as minus{'a} instead of sub{'a}.
      - Rewrote Yegor's theories to use the parser shortcut for "minus".
      - Fixed the minus_df.