changeset 7118 | ee384c7b7416 |
parent 7093 | b2ee0e5d1a7f |
child 7166 | a4a870ec2e67 |
--- 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")]; +