--- a/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 21:10:01 2024 +0200
@@ -1006,6 +1006,9 @@
syntax
"_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
+syntax_consts
+ "_almost_everywhere" \<rightleftharpoons> almost_everywhere
+
translations
"AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"
@@ -1016,6 +1019,9 @@
"_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
("AE _\<in>_ in _./ _" [0,0,0,10] 10)
+syntax_consts
+ "_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere
+
translations
"AE x\<in>A in M. P" \<rightleftharpoons> "CONST set_almost_everywhere A M (\<lambda>x. P)"