1.1 --- a/src/Sequents/ILL.thy	Wed May 19 11:41:58 2004 +0200
     1.2 +++ b/src/Sequents/ILL.thy	Fri May 21 21:14:18 2004 +0200
     1.3 @@ -8,12 +8,7 @@
     1.4  ILL = Sequents +
     1.5  
     1.6  consts
     1.7 -
     1.8 -  
     1.9 - Trueprop	:: "two_seqi"
    1.10 - "@Trueprop"	:: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
    1.11 - 
    1.12 - 
    1.13 +  Trueprop       :: "two_seqi"
    1.14  
    1.15  "><"    ::"[o, o] => o"        (infixr 35)
    1.16  "-o"    ::"[o, o] => o"        (infixr 45)
    1.17 @@ -27,15 +22,18 @@
    1.18  aneg    ::"o=>o"               ("~_")
    1.19  
    1.20  
    1.21 -  (* syntax for context manipulation *)
    1.22 +  (* context manipulation *)
    1.23  
    1.24   Context      :: "two_seqi"
    1.25 -"@Context"    :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    1.26  
    1.27 -  (* syntax for promotion rule *)
    1.28 +  (* promotion rule *)
    1.29  
    1.30    PromAux :: "three_seqi"
    1.31 -"@PromAux":: "three_seqe" ("promaux {_||_||_}")
    1.32 +
    1.33 +syntax
    1.34 +  "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
    1.35 +  "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    1.36 +  "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    1.37  
    1.38  defs
    1.39  
    1.40 @@ -47,7 +45,7 @@
    1.41  
    1.42  
    1.43  rules
    1.44 -  
    1.45 +
    1.46  identity        "P |- P"
    1.47  
    1.48  zerol           "$G, 0, $H |- A"
    1.49 @@ -58,7 +56,7 @@
    1.50    (* unfortunately, this one removes !A  *)
    1.51  
    1.52  contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    1.53 -  
    1.54 +
    1.55  weaken     "$F, $G |- C ==> $G, !A, $F |- C"
    1.56    (* weak form of weakening, in practice just to clean context *)
    1.57    (* weaken and contract not needed (CHECK)  *)
    1.58 @@ -69,7 +67,7 @@
    1.59  promote0        "$G |- A ==> promaux {$G || || A}"
    1.60  
    1.61  
    1.62 -  
    1.63 +
    1.64  tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    1.65  
    1.66  impr      "A, $F |- B ==> $F |- A -o B"
    1.67 @@ -101,7 +99,7 @@
    1.68                         $G |- A |]
    1.69                      ==> $J, A -o B, $H |- C"
    1.70  
    1.71 -    
    1.72 +
    1.73  cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
    1.74           $H1, $H2, $H3, $H4 |- A ;
    1.75           $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
    1.76 @@ -118,7 +116,7 @@
    1.77  
    1.78  
    1.79  
    1.80 - 
    1.81 +
    1.82  end
    1.83  
    1.84  ML
    1.85 @@ -131,4 +129,4 @@
    1.86                           ("Context",Sequents.two_seq_tr'"@Context"),
    1.87                           ("PromAux", Sequents.three_seq_tr'"@PromAux")];
    1.88  
    1.89 - 
    1.90 +