--- a/src/HOL/Analysis/Set_Integral.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Sep 20 19:51:08 2024 +0200
@@ -24,7 +24,7 @@
syntax
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- ("(4LINT (_):(_)/|(_)./ _)" [0,0,0,10] 10)
+ (\<open>(4LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
syntax_consts
"_ascii_set_lebesgue_integral" == set_lebesgue_integral
@@ -43,11 +43,11 @@
syntax
"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
- ("(2LBINT _./ _)" [0,10] 10)
+ (\<open>(2LBINT _./ _)\<close> [0,10] 10)
syntax
"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
- ("(3LBINT _:_./ _)" [0,0,10] 10)
+ (\<open>(3LBINT _:_./ _)\<close> [0,0,10] 10)
section \<open>Basic properties\<close>
@@ -572,12 +572,12 @@
abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
"complex_integrable M f \<equiv> integrable M f"
-abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
+abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" (\<open>integral\<^sup>C\<close>) where
"integral\<^sup>C M f == integral\<^sup>L M f"
syntax
"_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
- ("\<integral>\<^sup>C _. _ \<partial>_" [0,0] 110)
+ (\<open>\<integral>\<^sup>C _. _ \<partial>_\<close> [0,0] 110)
syntax_consts
"_complex_lebesgue_integral" == complex_lebesgue_integral
@@ -587,7 +587,7 @@
syntax
"_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- ("(3CLINT _|_. _)" [0,0,10] 10)
+ (\<open>(3CLINT _|_. _)\<close> [0,0,10] 10)
syntax_consts
"_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
@@ -624,7 +624,7 @@
syntax
"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- ("(4CLINT _:_|_. _)" [0,0,0,10] 10)
+ (\<open>(4CLINT _:_|_. _)\<close> [0,0,0,10] 10)
syntax_consts
"_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
@@ -647,10 +647,10 @@
syntax
"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,0,0,110] 10)
+(\<open>(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,0,0,110] 10)
+(\<open>(\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
syntax_consts
"_set_nn_integral" == set_nn_integral and