diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Homotopy.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -3340,7 +3340,7 @@
 subsection\<open>Homotopy equivalence of topological spaces.\<close>
 
 definition\<^marker>\<open>tag important\<close> homotopy_equivalent_space
-             (infix "homotopy'_equivalent'_space" 50)
+             (infix \<open>homotopy'_equivalent'_space\<close> 50)
   where "X homotopy_equivalent_space Y \<equiv>
         (\<exists>f g. continuous_map X Y f \<and>
               continuous_map Y X g \<and>
@@ -3781,7 +3781,7 @@
 
 
 abbreviation\<^marker>\<open>tag important\<close> homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
-             (infix "homotopy'_eqv" 50)
+             (infix \<open>homotopy'_eqv\<close> 50)
   where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
 
 lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"