--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 21:10:01 2024 +0200
@@ -586,6 +586,9 @@
syntax
"_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110)
+syntax_consts
+ "_simple_integral" == simple_integral
+
translations
"\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)"
@@ -819,6 +822,9 @@
syntax
"_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110)
+syntax_consts
+ "_nn_integral" == nn_integral
+
translations
"\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"