diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Induct/Comb.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -20,14 +20,14 @@
 
 datatype comb = K
               | S
-              | Ap comb comb (infixl "\<bullet>" 90)
+              | Ap comb comb (infixl \<open>\<bullet>\<close> 90)
 
 text \<open>
   Inductive definition of contractions, \<open>\<rightarrow>\<^sup>1\<close> and
   (multi-step) reductions, \<open>\<rightarrow>\<close>.
 \<close>
 
-inductive contract1 :: "[comb,comb] \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sup>1" 50)
+inductive contract1 :: "[comb,comb] \<Rightarrow> bool"  (infixl \<open>\<rightarrow>\<^sup>1\<close> 50)
   where
     K:     "K\<bullet>x\<bullet>y \<rightarrow>\<^sup>1 x"
   | S:     "S\<bullet>x\<bullet>y\<bullet>z \<rightarrow>\<^sup>1 (x\<bullet>z)\<bullet>(y\<bullet>z)"
@@ -35,7 +35,7 @@
   | Ap2:   "x \<rightarrow>\<^sup>1 y \<Longrightarrow> z\<bullet>x \<rightarrow>\<^sup>1 z\<bullet>y"
 
 abbreviation
-  contract :: "[comb,comb] \<Rightarrow> bool"   (infixl "\<rightarrow>" 50) where
+  contract :: "[comb,comb] \<Rightarrow> bool"   (infixl \<open>\<rightarrow>\<close> 50) where
   "contract \<equiv> contract1\<^sup>*\<^sup>*"
 
 text \<open>
@@ -43,7 +43,7 @@
   (multi-step) parallel reductions, \<open>\<Rrightarrow>\<close>.
 \<close>
 
-inductive parcontract1 :: "[comb,comb] \<Rightarrow> bool"  (infixl "\<Rrightarrow>\<^sup>1" 50)
+inductive parcontract1 :: "[comb,comb] \<Rightarrow> bool"  (infixl \<open>\<Rrightarrow>\<^sup>1\<close> 50)
   where
     refl:  "x \<Rrightarrow>\<^sup>1 x"
   | K:     "K\<bullet>x\<bullet>y \<Rrightarrow>\<^sup>1 x"
@@ -51,7 +51,7 @@
   | Ap:    "\<lbrakk>x \<Rrightarrow>\<^sup>1 y; z \<Rrightarrow>\<^sup>1 w\<rbrakk> \<Longrightarrow> x\<bullet>z \<Rrightarrow>\<^sup>1 y\<bullet>w"
 
 abbreviation
-  parcontract :: "[comb,comb] \<Rightarrow> bool"   (infixl "\<Rrightarrow>" 50) where
+  parcontract :: "[comb,comb] \<Rightarrow> bool"   (infixl \<open>\<Rrightarrow>\<close> 50) where
   "parcontract \<equiv> parcontract1\<^sup>*\<^sup>*"
 
 text \<open>