author Andreas Lochbihler Wed, 14 Jan 2015 10:15:41 +0100 changeset 59357 f366643536cd parent 59356 e6f5b1bbcb01 child 59358 7fd531cc0172
allow line breaks in integral notation
```--- 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)"```