diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/NanoJava/OpSem.thy
--- a/src/HOL/NanoJava/OpSem.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -8,8 +8,8 @@
 theory OpSem imports State begin
 
 inductive
-  exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
-  and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
+  exec :: "[state,stmt,    nat,state] => bool" (\<open>_ -_-_\<rightarrow> _\<close>  [98,90,   65,98] 89)
+  and eval :: "[state,expr,val,nat,state] => bool" (\<open>_ -_\<succ>_-_\<rightarrow> _\<close>[98,95,99,65,98] 89)
 where
   Skip: "   s -Skip-n\<rightarrow> s"