# HG changeset patch
# User Andreas Lochbihler
# Date 1421226941 -3600
# Node ID f366643536cd2e9550547d232485eb08c34a7464
# Parent  e6f5b1bbcb01e3060552d5d04c7aaf61944a0b87
allow line breaks in integral notation

diff -r e6f5b1bbcb01 -r f366643536cd src/HOL/Probability/Bochner_Integration.thy
--- 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)"
diff -r e6f5b1bbcb01 -r f366643536cd src/HOL/Probability/Lebesgue_Measure.thy
--- 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
diff -r e6f5b1bbcb01 -r f366643536cd src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- 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)"