--- a/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 21:10:01 2024 +0200
@@ -148,6 +148,9 @@
"_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
+syntax_consts
+ "_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
+
translations
"LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
@@ -159,6 +162,9 @@
"_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
("(4LBINT _=_.._. _)" [0,60,60,61] 60)
+syntax_consts
+ "_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
+
translations
"LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
@@ -1045,11 +1051,17 @@
syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
("(2CLBINT _. _)" [0,60] 60)
+syntax_consts
+ "_complex_lebesgue_borel_integral" == complex_lebesgue_integral
+
translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
("(3CLBINT _:_. _)" [0,60,61] 60)
+syntax_consts
+ "_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
+
translations
"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
@@ -1065,6 +1077,9 @@
"_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
+syntax_consts
+ "_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
+
translations
"CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"