diff -r 46f59511b7bb -r d97fdabd9e2b src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/Doc/Codegen/Introduction.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -123,11 +123,11 @@
 \<close>
 
 class %quote semigroup =
-  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
+  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>\<otimes>\<close> 70)
   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
 
 class %quote monoid = semigroup +
-  fixes neutral :: 'a ("\<one>")
+  fixes neutral :: 'a (\<open>\<one>\<close>)
   assumes neutl: "\<one> \<otimes> x = x"
     and neutr: "x \<otimes> \<one> = x"