src/Sequents/Modal0.thy
changeset 69605 3dda49e08b9d
parent 62144 bdab93ccfaf8
child 69618 a96320074298
--- a/src/Sequents/Modal0.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Sequents/Modal0.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -25,13 +25,13 @@
 \<close>
 
 parse_translation \<open>
- [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
-  (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
+ [(\<^syntax_const>\<open>_Lstar\<close>, K (star_tr \<^const_syntax>\<open>Lstar\<close>)),
+  (\<^syntax_const>\<open>_Rstar\<close>, K (star_tr \<^const_syntax>\<open>Rstar\<close>))]
 \<close>
 
 print_translation \<open>
- [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
-  (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
+ [(\<^const_syntax>\<open>Lstar\<close>, K (star_tr' \<^syntax_const>\<open>_Lstar\<close>)),
+  (\<^const_syntax>\<open>Rstar\<close>, K (star_tr' \<^syntax_const>\<open>_Rstar\<close>))]
 \<close>
 
 definition strimp :: "[o,o]\<Rightarrow>o"   (infixr "--<" 25)