src/HOL/Analysis/Interval_Integral.thy

   "interval_lebesgue_integral M a b f =
     (if a \<le> b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))"
 
 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
 
 translations

   "interval_lebesgue_integrable M a b f =
     (if a \<le> b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)"
 
 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
 
 translations

     by (simp add: ac_simps)
 qed
 
 
 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
 
 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
 
 translations

   "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" where
   "complex_interval_lebesgue_integrable M a b f \<equiv> interval_lebesgue_integrable M a b f"
 
 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
 
 translations