diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/IMP/VCG_Total_EX.thy
--- a/src/HOL/IMP/VCG_Total_EX.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/IMP/VCG_Total_EX.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -12,14 +12,14 @@
 invariants.\<close>
 
 datatype acom =
-  Askip                  ("SKIP") |
-  Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
-  Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
-  Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
+  Askip                  (\<open>SKIP\<close>) |
+  Aassign vname aexp     (\<open>(_ ::= _)\<close> [1000, 61] 61) |
+  Aseq   acom acom       (\<open>_;;/ _\<close>  [60, 61] 60) |
+  Aif bexp acom acom     (\<open>(IF _/ THEN _/ ELSE _)\<close>  [0, 0, 61] 61) |
   Awhile "nat \<Rightarrow> assn" bexp acom
-    ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
+    (\<open>({_}/ WHILE _/ DO _)\<close>  [0, 0, 61] 61)
 
-notation com.SKIP ("SKIP")
+notation com.SKIP (\<open>SKIP\<close>)
 
 text\<open>Strip annotations:\<close>