# HG changeset patch
# User Andreas Lochbihler
# Date 1421239894 -3600
# Node ID 7fd531cc0172b04f25eaf3c740b6764e055ab5ee
# Parent  f366643536cd2e9550547d232485eb08c34a7464
more line breaks in integral notation

diff -r f366643536cd -r 7fd531cc0172 src/HOL/Probability/Set_Integral.thy
--- a/src/HOL/Probability/Set_Integral.thy	Wed Jan 14 10:15:41 2015 +0100
+++ b/src/HOL/Probability/Set_Integral.thy	Wed Jan 14 13:51:34 2015 +0100
@@ -16,7 +16,7 @@
 
 syntax
 "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(3LINT _|_. _)" [0,110,60] 60)
+("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
 
 translations
 "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
@@ -29,7 +29,7 @@
 
 syntax
 "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4LINT _:_|_. _)" [0,60,110,61] 60)
+("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
 
 translations
 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
@@ -39,7 +39,7 @@
 
 syntax
   "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
-("AE _\<in>_ in _. _" [0,0,0,10] 10)
+("AE _\<in>_ in _./ _" [0,0,0,10] 10)
 
 translations
   "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
@@ -55,14 +55,14 @@
 
 syntax
 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-("(2LBINT _. _)" [0,60] 60)
+("(2LBINT _./ _)" [0,60] 60)
 
 translations
 "LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
 
 syntax
 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-("(3LBINT _:_. _)" [0,60,61] 60)
+("(3LBINT _:_./ _)" [0,60,61] 60)
 
 translations
 "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"