diff -r 8c937127fd8c -r a4a870ec2e67 src/Sequents/LK0.thy
--- 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")];