--- a/src/HOL/Analysis/Measure_Space.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Sep 20 19:51:08 2024 +0200
@@ -1004,7 +1004,7 @@
"almost_everywhere M P \<equiv> eventually P (ae_filter M)"
syntax
- "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
+ "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" (\<open>AE _ in _. _\<close> [0,0,10] 10)
syntax_consts
"_almost_everywhere" \<rightleftharpoons> almost_everywhere
@@ -1017,7 +1017,7 @@
syntax
"_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
- ("AE _\<in>_ in _./ _" [0,0,0,10] 10)
+ (\<open>AE _\<in>_ in _./ _\<close> [0,0,0,10] 10)
syntax_consts
"_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere