Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-29 14:26:39 -0700 (Fri, 29 Jul 2005)
Revision: 7669
Log message:

      Now it seems to be capable of realizing S4 proof of box(a -> a) in LP.
      

Changes	Path
+1 -0	metaprl/theories/s4lp/hilbert_internal.mli
+116 -79	metaprl/theories/s4lp/s4_internal.ml