Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-15 16:25:29 -0700 (Fri, 15 Jul 2005)
Revision: 7617
Log message:

      finally it is smart enough to apply rules in the right order while proving
      K1 K2 p => K1 K2 K2 p
      

Changes	Path
+46 -33	metaprl/refiner/reflib/jall.ml
+276 -232	metaprl/theories/s4lp/s4_tests.prla