# HG changeset patch
# User paulson
# Date 1708098906 0
# Node ID 5bedeb0dc827b299ccfa10ddf343efd9567fc9a7
# Parent  4d81c0391da2af63638fa10be8eb7e288f429f6a# Parent  a8407aa7f9164dc044d1efd98f17390667e06d2d
merged

diff -r 4d81c0391da2 -r 5bedeb0dc827 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Fri Feb 16 11:25:11 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Feb 16 15:55:06 2024 +0000
@@ -23,7 +23,7 @@
 
 syntax
   "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 10)
+  ("(4LINT (_):(_)/|(_)./ _)" [0,0,0,10] 10)
 
 translations
   "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
@@ -39,11 +39,11 @@
 
 syntax
   "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-  ("(2LBINT _./ _)" [0,60] 10)
+  ("(2LBINT _./ _)" [0,10] 10)
 
 syntax
   "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-  ("(3LBINT _:_./ _)" [0,60,61] 10)
+  ("(3LBINT _:_./ _)" [0,0,10] 10)
 
 (*
     Basic properties
@@ -570,14 +570,14 @@
 
 syntax
   "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
- ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
+ ("\<integral>\<^sup>C _. _ \<partial>_" [0,0] 110)
 
 translations
   "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
 
 syntax
   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  ("(3CLINT _|_. _)" [0,110,60] 10)
+  ("(3CLINT _|_. _)" [0,0,10] 10)
 
 translations
   "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -611,7 +611,7 @@
 
 syntax
 "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4CLINT _:_|_. _)" [0,60,110,61] 10)
+("(4CLINT _:_|_. _)" [0,0,0,10] 10)
 
 translations
 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
@@ -630,10 +630,10 @@
 
 syntax
 "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 10)
+("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,0,0,110] 10)
 
 "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 10)
+("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,0,0,110] 10)
 
 translations
 "\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"