Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-28 18:15:46 -0700 (Thu, 28 Jul 2005)
Revision: 7668
Log message:

      Now box should be timely converted to proof terms, it's time to see how the whole thing works.
      

Changes	Path
+47 -30	metaprl/theories/s4lp/s4_internal.ml