--- a/src/Sequents/ILL.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/Sequents/ILL.thy Fri May 21 21:14:18 2004 +0200
@@ -8,12 +8,7 @@
ILL = Sequents +
consts
-
-
- Trueprop :: "two_seqi"
- "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
-
-
+ Trueprop :: "two_seqi"
"><" ::"[o, o] => o" (infixr 35)
"-o" ::"[o, o] => o" (infixr 45)
@@ -27,15 +22,18 @@
aneg ::"o=>o" ("~_")
- (* syntax for context manipulation *)
+ (* context manipulation *)
Context :: "two_seqi"
-"@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
- (* syntax for promotion rule *)
+ (* promotion rule *)
PromAux :: "three_seqi"
-"@PromAux":: "three_seqe" ("promaux {_||_||_}")
+
+syntax
+ "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
+ "@PromAux" :: "three_seqe" ("promaux {_||_||_}")
defs
@@ -47,7 +45,7 @@
rules
-
+
identity "P |- P"
zerol "$G, 0, $H |- A"
@@ -58,7 +56,7 @@
(* unfortunately, this one removes !A *)
contract "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
-
+
weaken "$F, $G |- C ==> $G, !A, $F |- C"
(* weak form of weakening, in practice just to clean context *)
(* weaken and contract not needed (CHECK) *)
@@ -69,7 +67,7 @@
promote0 "$G |- A ==> promaux {$G || || A}"
-
+
tensl "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
impr "A, $F |- B ==> $F |- A -o B"
@@ -101,7 +99,7 @@
$G |- A |]
==> $J, A -o B, $H |- C"
-
+
cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
$H1, $H2, $H3, $H4 |- A ;
$J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B"
@@ -118,7 +116,7 @@
-
+
end
ML
@@ -131,4 +129,4 @@
("Context",Sequents.two_seq_tr'"@Context"),
("PromAux", Sequents.three_seq_tr'"@PromAux")];
-
+