1.1 --- a/src/Sequents/S4.thy	Thu Feb 28 14:10:54 2013 +0100
     1.2 +++ b/src/Sequents/S4.thy	Thu Feb 28 14:22:14 2013 +0100
     1.3 @@ -7,26 +7,26 @@
     1.4  imports Modal0
     1.5  begin
     1.6  
     1.7 -axioms
     1.8 +axiomatization where
     1.9  (* Definition of the star operation using a set of Horn clauses *)
    1.10  (* For system S4:  gamma * == {[]P | []P : gamma}               *)
    1.11  (*                 delta * == {<>P | <>P : delta}               *)
    1.12  
    1.13 -  lstar0:         "|L>"
    1.14 -  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
    1.15 -  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
    1.16 -  rstar0:         "|R>"
    1.17 -  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    1.18 -  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
    1.19 +  lstar0:         "|L>" and
    1.20 +  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
    1.21 +  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
    1.22 +  rstar0:         "|R>" and
    1.23 +  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
    1.24 +  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
    1.25  
    1.26  (* Rules for [] and <> *)
    1.27  
    1.28    boxR:
    1.29     "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
    1.30 -           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    1.31 -  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    1.32 +           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
    1.33 +  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G" and
    1.34  
    1.35 -  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    1.36 +  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G" and
    1.37    diaL:
    1.38     "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    1.39             $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"