diff -r 37eccadf6b8a -r ee384c7b7416 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Wed Jul 28 13:45:33 1999 +0200
+++ b/src/Sequents/LK0.thy	Wed Jul 28 13:45:54 1999 +0200
@@ -136,7 +136,11 @@
 
 end
 
-  ML
+ML
+
+fun side_tr [s1] = Sequents.seq_tr s1;
 
-val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
+val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop"),
+			 ("@Side", side_tr)];
 val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
+