diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -311,7 +311,7 @@
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close>
 
-definition constant_on  (infixl "(constant'_on)" 50)
+definition constant_on  (infixl \<open>(constant'_on)\<close> 50)
   where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
 
 lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
@@ -892,7 +892,7 @@
 where "retraction S T r \<longleftrightarrow>
   T \<subseteq> S \<and> continuous_on S r \<and> r \<in> S \<rightarrow> T \<and> (\<forall>x\<in>T. r x = x)"
 
-definition\<^marker>\<open>tag important\<close> retract_of (infixl "retract'_of" 50) where
+definition\<^marker>\<open>tag important\<close> retract_of (infixl \<open>retract'_of\<close> 50) where
 "T retract_of S  \<longleftrightarrow>  (\<exists>r. retraction S T r)"
 
 lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
@@ -1111,7 +1111,7 @@
 
 subsection\<open>Retractions on a topological space\<close>
 
-definition retract_of_space :: "'a set \<Rightarrow> 'a topology \<Rightarrow> bool" (infix "retract'_of'_space" 50)
+definition retract_of_space :: "'a set \<Rightarrow> 'a topology \<Rightarrow> bool" (infix \<open>retract'_of'_space\<close> 50)
   where "S retract_of_space X
          \<equiv> S \<subseteq> topspace X \<and> (\<exists>r. continuous_map X (subtopology X S) r \<and> (\<forall>x \<in> S. r x = x))"