src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy

   "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"
 
 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)"
 
 lemma simple_integral_cong:
   assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"

 definition\<^marker>\<open>tag important\<close> nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where
   "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
 
 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)"
 
 lemma nn_integral_def_finite: