--- a/src/HOL/Probability/Bochner_Integration.thy Wed Jan 14 09:59:12 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Wed Jan 14 10:15:41 2015 +0100
@@ -893,7 +893,7 @@
"integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
syntax
- "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral> _. _ \<partial>_" [60,61] 110)
+ "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral>((2 _./ _)/ \<partial>_)" [60,61] 110)
translations
"\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Jan 14 09:59:12 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Jan 14 10:15:41 2015 +0100
@@ -5,7 +5,7 @@
Author: Luke Serafin
*)
-section {* Lebsegue measure *}
+section {* Lebesgue measure *}
theory Lebesgue_Measure
imports Finite_Product_Measure Bochner_Integration Caratheodory
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Jan 14 09:59:12 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Jan 14 10:15:41 2015 +0100
@@ -740,7 +740,7 @@
"integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
syntax
- "_nn_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
+ "_nn_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110)
translations
"\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"