diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/S43.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -32,17 +32,17 @@
 in [(@{const_syntax S43pi}, s43pi_tr')] end
 *}
 
-axioms
+axiomatization where
 (* Definition of the star operation using a set of Horn clauses  *)
 (* For system S43: gamma * == {[]P | []P : gamma}                *)
 (*                 delta * == {<>P | <>P : delta}                *)
 
-  lstar0:         "|L>"
-  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
-  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
-  rstar0:         "|R>"
-  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
-  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
+  lstar0:         "|L>" and
+  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
+  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
+  rstar0:         "|R>" and
+  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
+  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
 
 (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
 (* ie                                                                        *)
@@ -54,22 +54,22 @@
 (*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
 (*    and 1<=i<=k and k<j<=k+m                                               *)
 
-  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia"
+  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia" and
   S43pi1:
    "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==>
-       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
+       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia" and
   S43pi2:
    "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==>
-       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
+       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia" and
 
 (* Rules for [] and <> for S43 *)
 
-  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
-  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
+  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and
+  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and
   pi1:
    "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
       S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
-   $L1, <>P, $L2 |- $R"
+   $L1, <>P, $L2 |- $R" and
   pi2:
    "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
       S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>