--- a/src/Sequents/LK0.thy Tue Aug 03 13:15:54 1999 +0200
+++ b/src/Sequents/LK0.thy Tue Aug 03 13:16:29 1999 +0200
@@ -24,9 +24,6 @@
Trueprop :: "two_seqi"
"@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
- (*Constant to allow definitions of SEQUENCES of formulas*)
- "@Side" :: "seq=>(seq'=>seq')" ("<<(_)>>")
-
True,False :: o
"=" :: ['a,'a] => o (infixl 50)
Not :: o => o ("~ _" [40] 40)
@@ -138,9 +135,7 @@
ML
-fun side_tr [s1] = Sequents.seq_tr s1;
-val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop"),
- ("@Side", side_tr)];
+val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];