Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-01-25 00:05:22 -0800 (Thu, 25 Jan 2001)
Revision: 3108
Log message:

      
      Now each rewrite has rewrite- and '~'- forms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-01-25 10:49:45 -0800 (Thu, 25 Jan 2001)
Revision: 3109
Log message:

      Fixed the types for topval conversions, uncommented them in the .mli file.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-01-26 13:15:20 -0800 (Fri, 26 Jan 2001)
Revision: 3115
Log message:

      I have added a new theory Itt_struct2 with some derived advanced versions of
      substitution rules and the cut rule.
      In particular, I have proved the let (cutEq) rule (that is the cut rule for the membership).
      
      Itt_struct2 redefines the substT tactic to use stronger substitution rules.
      There are also new tactics: letT, assetEqT and assertHideT.
      
      Itt_theory does not include Itt_struct2. If you whant to use these rules, you need to include
      Itt_struct2 explicitly.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-01-26 14:08:07 -0800 (Fri, 26 Jan 2001)
Revision: 3116
Log message:

      Clean proofs in itt_bunion.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2001-01-28 16:16:41 -0800 (Sun, 28 Jan 2001)
Revision: 3117
Log message:

      Data types for unification with lasy convertion of terms
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-01-29 13:06:02 -0800 (Mon, 29 Jan 2001)
Revision: 3118
Log message:

      Added links to MetaPRL CVS Logs and the theories.pdf
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-01-29 13:13:54 -0800 (Mon, 29 Jan 2001)
Revision: 3119
Log message:

      More documentation links.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-01-29 13:23:46 -0800 (Mon, 29 Jan 2001)
Revision: 3120
Log message:

      .
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-01-29 17:05:43 -0800 (Mon, 29 Jan 2001)
Revision: 3121
Log message:

      1. I removed an invalid rule from itt_isect,
      derived some rule that was primitive, and
      added some new derivable rules on intersection
      (see theories.pdf).
      
      2. Fix a bug in Itt_struct2.
      
      3. Now Itt_isect and Itt_theory include Itt_struct2
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-01-30 11:31:25 -0800 (Tue, 30 Jan 2001)
Revision: 3122
Log message:

      Minor changes.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-01-31 12:23:20 -0800 (Wed, 31 Jan 2001)
Revision: 3123
Log message:

      There was inconsistent with the documentation and the implementation
      of the ifLabT and RepeatT tactics.
      
      The documentation about ifLabT is corrected.
      
      The old repeatT tactic is now called whileProgressT.
      
      The (repeatT tac)  is now defined as whileProgressT (tryT tac)
      
      Still to do: implement the untilFailT tactic (Nuprl's REPEAT).
      
      
      * whileProgressT : tactic -> tactic
      Repeatedly execute the given tactic on all subgoals while there is a progress.
      
      * untilFailT : tactic -> tactic
      Repeatedly execute the given tactic on all subgoals until it fails.
      
      * repeatT : tactic -> tactic
      Repeatedly execute the given tactic on all subgoals until it fails or no more
      progress is made.
      
      See also all-theories.pdf.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-01-31 14:44:31 -0800 (Wed, 31 Jan 2001)
Revision: 3124
Log message:

      Spelling changes.
      For best results, upgrade to http://www.cs.cornell.edu/nogin/RPM/MetaPRL/noarch/words-2.1-1.noarch.html
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-01-31 17:18:20 -0800 (Wed, 31 Jan 2001)
Revision: 3125
Log message:

      1. The untilFailT tactical is implemented.
      
      2. Now there are the untilFailC, whileProgressC and repeatC conversionals
      hat work as corresponding tacticals.
      
      3. The failC a failWithC conversions now work as failT and failWithT
      
      4. repeatForT and repeatForC now raise an exception when applied to
      a negative argument.