--- a/src/HOL/Analysis/Interval_Integral.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Sep 20 19:51:08 2024 +0200
@@ -146,7 +146,7 @@
syntax
"_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
- ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
+ (\<open>(5LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
syntax_consts
"_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
@@ -160,7 +160,7 @@
syntax
"_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
- ("(4LBINT _=_.._. _)" [0,60,60,61] 60)
+ (\<open>(4LBINT _=_.._. _)\<close> [0,60,60,61] 60)
syntax_consts
"_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
@@ -1049,7 +1049,7 @@
syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
- ("(2CLBINT _. _)" [0,60] 60)
+ (\<open>(2CLBINT _. _)\<close> [0,60] 60)
syntax_consts
"_complex_lebesgue_borel_integral" == complex_lebesgue_integral
@@ -1057,7 +1057,7 @@
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)
+ (\<open>(3CLBINT _:_. _)\<close> [0,60,61] 60)
syntax_consts
"_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
@@ -1075,7 +1075,7 @@
syntax
"_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
- ("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
+ (\<open>(4CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
syntax_consts
"_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral