diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Sparse_In.thy
--- a/src/HOL/Analysis/Sparse_In.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -10,7 +10,7 @@
 subsection \<open>A set of points sparse in another set\<close>
 
 definition sparse_in:: "'a :: topological_space set \<Rightarrow> 'a set \<Rightarrow> bool"
-    (infixl "(sparse'_in)" 50)
+    (infixl \<open>(sparse'_in)\<close> 50)
   where
   "pts sparse_in A = (\<forall>x\<in>A. \<exists>B. x\<in>B \<and> open B \<and> (\<forall>y\<in>B. \<not> y islimpt pts))"
 
@@ -165,14 +165,14 @@
  "cosparse A = Abs_filter (\<lambda>P. {x. \<not>P x} sparse_in A)"
 
 syntax
-  "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  ("(3\<forall>\<^sub>\<approx>_\<in>_./ _)" [0, 0, 10] 10)
+  "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  (\<open>(3\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_eventually_cosparse" == eventually
 translations
   "\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
 
 syntax
-  "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3\<forall>\<^sub>\<approx>_ | (_)./ _)" [0, 0, 10] 10)
+  "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_qeventually_cosparse" == eventually
 translations