diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -28,7 +28,7 @@
   where "reversepath g \<equiv> (\<lambda>x. g(1 - x))"
 
 definition\<^marker>\<open>tag important\<close> joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
-    (infixr "+++" 75)
+    (infixr \<open>+++\<close> 75)
   where "g1 +++ g2 \<equiv> (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
 
 definition\<^marker>\<open>tag important\<close> loop_free :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"