diff -r f6e595e4f608 -r 261cd8722677 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Filter.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -40,7 +40,7 @@
   where "eventually P F \<longleftrightarrow> Rep_filter F P"
 
 syntax
-  "_eventually" :: "pttrn => 'a filter => bool => bool"  ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+  "_eventually" :: "pttrn => 'a filter => bool => bool"  (\<open>(3\<forall>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_eventually" == eventually
 translations
@@ -160,7 +160,7 @@
   where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
 
 syntax
-  "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+  "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(3\<exists>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_frequently" == frequently
 translations
@@ -1033,15 +1033,15 @@
 
 definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
 
-abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>\<^sub>\<infinity>" 10)
+abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder \<open>\<exists>\<^sub>\<infinity>\<close> 10)
   where "Inf_many P \<equiv> frequently P cofinite"
 
-abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>\<^sub>\<infinity>" 10)
+abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder \<open>\<forall>\<^sub>\<infinity>\<close> 10)
   where "Alm_all P \<equiv> eventually P cofinite"
 
 notation (ASCII)
-  Inf_many  (binder "INFM " 10) and
-  Alm_all  (binder "MOST " 10)
+  Inf_many  (binder \<open>INFM \<close> 10) and
+  Alm_all  (binder \<open>MOST \<close> 10)
 
 lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
   unfolding cofinite_def
@@ -1080,7 +1080,7 @@
 
 subsubsection \<open>Product of filters\<close>
 
-definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr "\<times>\<^sub>F" 80) where
+definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr \<open>\<times>\<^sub>F\<close> 80) where
   "prod_filter F G =
     (\<Sqinter>(P, Q)\<in>{(P, Q). eventually P F \<and> eventually Q G}. principal {(x, y). P x \<and> Q y})"
 
@@ -1307,7 +1307,7 @@
   "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
 
 syntax
-  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
+  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(3LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
 
 syntax_consts
   "_LIM" == filterlim