Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adding missing declarations for the <<...>> notation
authorpaulson
Wed, 28 Jul 1999 13:45:54 +0200
changeset 7118 ee384c7b7416
parent 7117 37eccadf6b8a
child 7119 02d94b69ae04
adding missing declarations for the <<...>> notation
src/Sequents/LK0.thy file | annotate | diff | comparison | revisions 
--- 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")];
+
isabelle