diff -r f6e595e4f608 -r 261cd8722677 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Series.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -16,14 +16,14 @@
 subsection \<open>Definition of infinite summability\<close>
 
 definition sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
-    (infixr "sums" 80)
+    (infixr \<open>sums\<close> 80)
   where "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s"
 
 definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool"
   where "summable f \<longleftrightarrow> (\<exists>s. f sums s)"
 
 definition suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a"
-    (binder "\<Sum>" 10)
+    (binder \<open>\<Sum>\<close> 10)
   where "suminf f = (THE s. f sums s)"
 
 text\<open>Variants of the definition\<close>