1.1 --- a/src/Sequents/ILL.thy	Thu Feb 28 14:10:54 2013 +0100
     1.2 +++ b/src/Sequents/ILL.thy	Thu Feb 28 14:22:14 2013 +0100
     1.3 @@ -54,47 +54,47 @@
     1.4  aneg_def:        "~A == A -o 0"
     1.5  
     1.6  
     1.7 -axioms
     1.8 +axiomatization where
     1.9  
    1.10 -identity:        "P |- P"
    1.11 +identity:        "P |- P" and
    1.12  
    1.13 -zerol:           "$G, 0, $H |- A"
    1.14 +zerol:           "$G, 0, $H |- A" and
    1.15  
    1.16    (* RULES THAT DO NOT DIVIDE CONTEXT *)
    1.17  
    1.18 -derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
    1.19 +derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C" and
    1.20    (* unfortunately, this one removes !A  *)
    1.21  
    1.22 -contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    1.23 +contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" and
    1.24  
    1.25 -weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
    1.26 +weaken:     "$F, $G |- C ==> $G, !A, $F |- C" and
    1.27    (* weak form of weakening, in practice just to clean context *)
    1.28    (* weaken and contract not needed (CHECK)  *)
    1.29  
    1.30 -promote2:        "promaux{ || $H || B} ==> $H |- !B"
    1.31 +promote2:        "promaux{ || $H || B} ==> $H |- !B" and
    1.32  promote1:        "promaux{!A, $G || $H || B}
    1.33 -                  ==> promaux {$G || $H, !A || B}"
    1.34 -promote0:        "$G |- A ==> promaux {$G || || A}"
    1.35 +                  ==> promaux {$G || $H, !A || B}" and
    1.36 +promote0:        "$G |- A ==> promaux {$G || || A}" and
    1.37  
    1.38  
    1.39  
    1.40 -tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    1.41 +tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" and
    1.42  
    1.43 -impr:      "A, $F |- B ==> $F |- A -o B"
    1.44 +impr:      "A, $F |- B ==> $F |- A -o B" and
    1.45  
    1.46  conjr:           "[| $F |- A ;
    1.47                   $F |- B |]
    1.48 -                ==> $F |- (A && B)"
    1.49 +                ==> $F |- (A && B)" and
    1.50  
    1.51 -conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    1.52 +conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C" and
    1.53  
    1.54 -conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    1.55 +conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C" and
    1.56  
    1.57 -disjrl:          "$G |- A ==> $G |- A ++ B"
    1.58 -disjrr:          "$G |- B ==> $G |- A ++ B"
    1.59 +disjrl:          "$G |- A ==> $G |- A ++ B" and
    1.60 +disjrr:          "$G |- B ==> $G |- A ++ B" and
    1.61  disjl:           "[| $G, A, $H |- C ;
    1.62                       $G, B, $H |- C |]
    1.63 -                 ==> $G, A ++ B, $H |- C"
    1.64 +                 ==> $G, A ++ B, $H |- C" and
    1.65  
    1.66  
    1.67        (* RULES THAT DIVIDE CONTEXT *)
    1.68 @@ -102,26 +102,26 @@
    1.69  tensr:           "[| $F, $J :=: $G;
    1.70                       $F |- A ;
    1.71                       $J |- B     |]
    1.72 -                     ==> $G |- A >< B"
    1.73 +                     ==> $G |- A >< B" and
    1.74  
    1.75  impl:            "[| $G, $F :=: $J, $H ;
    1.76                       B, $F |- C ;
    1.77                          $G |- A |]
    1.78 -                     ==> $J, A -o B, $H |- C"
    1.79 +                     ==> $J, A -o B, $H |- C" and
    1.80  
    1.81  
    1.82  cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
    1.83            $H1, $H2, $H3, $H4 |- A ;
    1.84 -          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
    1.85 +          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B" and
    1.86  
    1.87  
    1.88    (* CONTEXT RULES *)
    1.89  
    1.90 -context1:     "$G :=: $G"
    1.91 -context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
    1.92 -context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
    1.93 -context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
    1.94 -context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
    1.95 +context1:     "$G :=: $G" and
    1.96 +context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" and
    1.97 +context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" and
    1.98 +context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G" and
    1.99 +context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G" and
   1.100  context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
   1.101  
   1.102  

     2.1 --- a/src/Sequents/LK/Nat.thy	Thu Feb 28 14:10:54 2013 +0100
     2.2 +++ b/src/Sequents/LK/Nat.thy	Thu Feb 28 14:22:14 2013 +0100
     2.3 @@ -11,20 +11,22 @@
     2.4  
     2.5  typedecl nat
     2.6  arities nat :: "term"
     2.7 -consts  Zero :: nat      ("0")
     2.8 -        Suc :: "nat=>nat"
     2.9 -        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    2.10 -        add :: "[nat, nat] => nat"                (infixl "+" 60)
    2.11  
    2.12 -axioms
    2.13 +axiomatization
    2.14 +  Zero :: nat      ("0") and
    2.15 +  Suc :: "nat=>nat" and
    2.16 +  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    2.17 +where
    2.18    induct:  "[| $H |- $E, P(0), $F;
    2.19 -              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
    2.20 +              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" and
    2.21  
    2.22 -  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
    2.23 -  Suc_neq_0:   "|- Suc(m) ~= 0"
    2.24 -  rec_0:       "|- rec(0,a,f) = a"
    2.25 +  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n" and
    2.26 +  Suc_neq_0:   "|- Suc(m) ~= 0" and
    2.27 +  rec_0:       "|- rec(0,a,f) = a" and
    2.28    rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    2.29 -  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
    2.30 +
    2.31 +definition add :: "[nat, nat] => nat"  (infixl "+" 60)
    2.32 +  where "m + n == rec(m, n, %x y. Suc(y))"
    2.33  
    2.34  
    2.35  declare Suc_neq_0 [simp]

     3.1 --- a/src/Sequents/LK0.thy	Thu Feb 28 14:10:54 2013 +0100
     3.2 +++ b/src/Sequents/LK0.thy	Thu Feb 28 14:22:14 2013 +0100
     3.3 @@ -59,67 +59,69 @@
     3.4    Ex  (binder "\<exists>" 10) and
     3.5    not_equal  (infixl "\<noteq>" 50)
     3.6  
     3.7 -axioms
     3.8 +axiomatization where
     3.9  
    3.10    (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
    3.11  
    3.12 -  contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
    3.13 -  contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
    3.14 +  contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" and
    3.15 +  contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" and
    3.16  
    3.17 -  thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F"
    3.18 -  thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E"
    3.19 +  thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" and
    3.20 +  thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" and
    3.21  
    3.22 -  exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
    3.23 -  exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
    3.24 +  exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" and
    3.25 +  exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" and
    3.26  
    3.27 -  cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
    3.28 +  cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E" and
    3.29  
    3.30    (*Propositional rules*)
    3.31  
    3.32 -  basic: "$H, P, $G |- $E, P, $F"
    3.33 +  basic: "$H, P, $G |- $E, P, $F" and
    3.34  
    3.35 -  conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
    3.36 -  conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
    3.37 +  conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" and
    3.38 +  conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" and
    3.39  
    3.40 -  disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
    3.41 -  disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
    3.42 +  disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" and
    3.43 +  disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" and
    3.44  
    3.45 -  impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
    3.46 -  impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
    3.47 +  impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" and
    3.48 +  impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" and
    3.49  
    3.50 -  notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
    3.51 -  notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
    3.52 +  notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F" and
    3.53 +  notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E" and
    3.54  
    3.55 -  FalseL: "$H, False, $G |- $E"
    3.56 +  FalseL: "$H, False, $G |- $E" and
    3.57  
    3.58 -  True_def: "True == False-->False"
    3.59 +  True_def: "True == False-->False" and
    3.60    iff_def:  "P<->Q == (P-->Q) & (Q-->P)"
    3.61  
    3.62 +axiomatization where
    3.63    (*Quantifiers*)
    3.64  
    3.65 -  allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
    3.66 -  allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
    3.67 +  allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" and
    3.68 +  allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" and
    3.69  
    3.70 -  exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
    3.71 -  exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
    3.72 +  exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" and
    3.73 +  exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" and
    3.74  
    3.75    (*Equality*)
    3.76 -
    3.77 -  refl:  "$H |- $E, a=a, $F"
    3.78 -  subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
    3.79 +  refl:  "$H |- $E, a=a, $F" and
    3.80 +  subst: "\<And>G H E. $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
    3.81  
    3.82    (* Reflection *)
    3.83  
    3.84 -  eq_reflection:  "|- x=y ==> (x==y)"
    3.85 +axiomatization where
    3.86 +  eq_reflection:  "|- x=y ==> (x==y)" and
    3.87    iff_reflection: "|- P<->Q ==> (P==Q)"
    3.88  
    3.89    (*Descriptions*)
    3.90  
    3.91 +axiomatization where
    3.92    The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
    3.93            $H |- $E, P(THE x. P(x)), $F"
    3.94  
    3.95 -definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) where 
    3.96 -   "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
    3.97 +definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
    3.98 +  where "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
    3.99  
   3.100  
   3.101  (** Structural Rules on formulas **)

     4.1 --- a/src/Sequents/S4.thy	Thu Feb 28 14:10:54 2013 +0100
     4.2 +++ b/src/Sequents/S4.thy	Thu Feb 28 14:22:14 2013 +0100
     4.3 @@ -7,26 +7,26 @@
     4.4  imports Modal0
     4.5  begin
     4.6  
     4.7 -axioms
     4.8 +axiomatization where
     4.9  (* Definition of the star operation using a set of Horn clauses *)
    4.10  (* For system S4:  gamma * == {[]P | []P : gamma}               *)
    4.11  (*                 delta * == {<>P | <>P : delta}               *)
    4.12  
    4.13 -  lstar0:         "|L>"
    4.14 -  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
    4.15 -  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
    4.16 -  rstar0:         "|R>"
    4.17 -  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    4.18 -  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
    4.19 +  lstar0:         "|L>" and
    4.20 +  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
    4.21 +  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
    4.22 +  rstar0:         "|R>" and
    4.23 +  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
    4.24 +  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
    4.25  
    4.26  (* Rules for [] and <> *)
    4.27  
    4.28    boxR:
    4.29     "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
    4.30 -           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    4.31 -  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    4.32 +           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
    4.33 +  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G" and
    4.34  
    4.35 -  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    4.36 +  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G" and
    4.37    diaL:
    4.38     "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    4.39             $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"

     5.1 --- a/src/Sequents/S43.thy	Thu Feb 28 14:10:54 2013 +0100
     5.2 +++ b/src/Sequents/S43.thy	Thu Feb 28 14:22:14 2013 +0100
     5.3 @@ -32,17 +32,17 @@
     5.4  in [(@{const_syntax S43pi}, s43pi_tr')] end
     5.5  *}
     5.6  
     5.7 -axioms
     5.8 +axiomatization where
     5.9  (* Definition of the star operation using a set of Horn clauses  *)
    5.10  (* For system S43: gamma * == {[]P | []P : gamma}                *)
    5.11  (*                 delta * == {<>P | <>P : delta}                *)
    5.12  
    5.13 -  lstar0:         "|L>"
    5.14 -  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
    5.15 -  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
    5.16 -  rstar0:         "|R>"
    5.17 -  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    5.18 -  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
    5.19 +  lstar0:         "|L>" and
    5.20 +  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
    5.21 +  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
    5.22 +  rstar0:         "|R>" and
    5.23 +  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
    5.24 +  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
    5.25  
    5.26  (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
    5.27  (* ie                                                                        *)
    5.28 @@ -54,22 +54,22 @@
    5.29  (*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
    5.30  (*    and 1<=i<=k and k<j<=k+m                                               *)
    5.31  
    5.32 -  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia"
    5.33 +  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia" and
    5.34    S43pi1:
    5.35     "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==>
    5.36 -       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
    5.37 +       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia" and
    5.38    S43pi2:
    5.39     "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==>
    5.40 -       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
    5.41 +       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia" and
    5.42  
    5.43  (* Rules for [] and <> for S43 *)
    5.44  
    5.45 -  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
    5.46 -  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
    5.47 +  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and
    5.48 +  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and
    5.49    pi1:
    5.50     "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
    5.51        S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
    5.52 -   $L1, <>P, $L2 |- $R"
    5.53 +   $L1, <>P, $L2 |- $R" and
    5.54    pi2:
    5.55     "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
    5.56        S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>

     6.1 --- a/src/Sequents/T.thy	Thu Feb 28 14:10:54 2013 +0100
     6.2 +++ b/src/Sequents/T.thy	Thu Feb 28 14:22:14 2013 +0100
     6.3 @@ -7,25 +7,25 @@
     6.4  imports Modal0
     6.5  begin
     6.6  
     6.7 -axioms
     6.8 +axiomatization where
     6.9  (* Definition of the star operation using a set of Horn clauses *)
    6.10  (* For system T:  gamma * == {P | []P : gamma}                  *)
    6.11  (*                delta * == {P | <>P : delta}                  *)
    6.12  
    6.13 -  lstar0:         "|L>"
    6.14 -  lstar1:         "$G |L> $H ==> []P, $G |L> P, $H"
    6.15 -  lstar2:         "$G |L> $H ==>   P, $G |L>    $H"
    6.16 -  rstar0:         "|R>"
    6.17 -  rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H"
    6.18 -  rstar2:         "$G |R> $H ==>   P, $G |R>    $H"
    6.19 +  lstar0:         "|L>" and
    6.20 +  lstar1:         "$G |L> $H ==> []P, $G |L> P, $H" and
    6.21 +  lstar2:         "$G |L> $H ==>   P, $G |L>    $H" and
    6.22 +  rstar0:         "|R>" and
    6.23 +  rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H" and
    6.24 +  rstar2:         "$G |R> $H ==>   P, $G |R>    $H" and
    6.25  
    6.26  (* Rules for [] and <> *)
    6.27  
    6.28    boxR:
    6.29     "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
    6.30 -               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    6.31 -  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
    6.32 -  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
    6.33 +               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
    6.34 +  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G" and
    6.35 +  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G" and
    6.36    diaL:
    6.37     "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    6.38                 $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"

     7.1 --- a/src/Sequents/Washing.thy	Thu Feb 28 14:10:54 2013 +0100
     7.2 +++ b/src/Sequents/Washing.thy	Thu Feb 28 14:22:14 2013 +0100
     7.3 @@ -6,26 +6,25 @@
     7.4  imports ILL
     7.5  begin
     7.6  
     7.7 -consts
     7.8 -  dollar :: o
     7.9 -  quarter :: o
    7.10 -  loaded :: o
    7.11 -  dirty :: o
    7.12 -  wet :: o
    7.13 +axiomatization
    7.14 +  dollar :: o and
    7.15 +  quarter :: o and
    7.16 +  loaded :: o and
    7.17 +  dirty :: o and
    7.18 +  wet :: o and
    7.19    clean :: o
    7.20 -
    7.21 -axioms
    7.22 +where
    7.23    change:
    7.24 -  "dollar |- (quarter >< quarter >< quarter >< quarter)"
    7.25 +  "dollar |- (quarter >< quarter >< quarter >< quarter)" and
    7.26  
    7.27    load1:
    7.28 -  "quarter , quarter , quarter , quarter , quarter |- loaded"
    7.29 +  "quarter , quarter , quarter , quarter , quarter |- loaded" and
    7.30  
    7.31    load2:
    7.32 -  "dollar , quarter |- loaded"
    7.33 +  "dollar , quarter |- loaded" and
    7.34  
    7.35    wash:
    7.36 -  "loaded , dirty |- wet"
    7.37 +  "loaded , dirty |- wet" and
    7.38  
    7.39    dry:
    7.40    "wet, quarter , quarter , quarter |- clean"