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	Path
+21 -17	metaprl/editor/ml/shell_rewrite.ml