Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-04 18:33:07 -0700 (Mon, 04 Jul 2005)
Revision: 7555
Log message:

      1. assumptions were incorrectly ordering in and_intro, fixed.
      2. more examples, all working properly:
      
      box(a & b) => box a & box b
      box a & box b => box(a & b)
      box(a => a)
      box box(a => a)
      box a or box b => box(a or b)
      

Changes	Path
+17 -3	metaprl-branches/S4-jprover/theories/s4lp/s4_logic.ml
+3746 -3549	metaprl-branches/S4-jprover/theories/s4lp/s4_logic.prla