--- a/src/Sequents/Modal0.thy Thu Jul 23 14:20:51 2015 +0200
+++ b/src/Sequents/Modal0.thy Thu Jul 23 14:25:05 2015 +0200
@@ -21,20 +21,20 @@
"_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5)
"_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5)
-ML {*
+ML \<open>
fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
-*}
+\<close>
-parse_translation {*
+parse_translation \<open>
[(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
(@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
-*}
+\<close>
-print_translation {*
+print_translation \<open>
[(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
(@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
-*}
+\<close>
defs
strimp_def: "P --< Q == [](P --> Q)"