Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2000-12-13 04:04:15 -0800 (Wed, 13 Dec 2000)
Revision: 3091
Log message:

      Moved from old style conditional rewrites to rules with '~' operator instead of '<-->'.
      Just now all reduce resources are commented out.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-12-16 16:45:04 -0800 (Sat, 16 Dec 2000)
Revision: 3095
Log message:

      When converting conditional rewrites to meta-sequents, not only
      convert the rewrite itself into seuqents, but also convert
      the assumptions as well.
      
      P.S. I was very surprised to find out that such sensitive conversion
      takes place so far from the "trusted core" of the system.
      We need to finally implement refiner-base proof checking, this way
      we can be sure that we do not have anything sensitive outside of Refiner.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-12-23 12:27:37 -0800 (Sat, 23 Dec 2000)
Revision: 3098
Log message:

      Quick start with MetaPrl proof-editor -- short summary for beginners.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-12-23 12:38:23 -0800 (Sat, 23 Dec 2000)
Revision: 3099
Log message:

      The reference to editor/ml/QUICKSTART is added. It is a short summary for
      the beginners -- explains how to use the proof-editor.