# HG changeset patch
# User wenzelm
# Date 1729255029 -7200
# Node ID f270cd6ee185f92f8146c7051fae3775ee721e54
# Parent  10e3a30b2512c4474167bc1bbae1eade8a95423d
clarified syntax declarations: keep things together;

diff -r 10e3a30b2512 -r f270cd6ee185 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Oct 18 14:35:13 2024 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Oct 18 14:37:09 2024 +0200
@@ -882,11 +882,17 @@
 
 subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
 
+syntax
+  "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
+    (\<open>(\<open>indent=2 notation=\<open>binder LBINT\<close>\<close>LBINT _./ _)\<close> [0,10] 10)
+  "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
+    (\<open>(\<open>indent=3 notation=\<open>binder LBINT\<close>\<close>LBINT _:_./ _)\<close> [0,0,10] 10)
+syntax_consts
+  "_lebesgue_borel_integral" \<rightleftharpoons> lebesgue_integral and
+  "_set_lebesgue_borel_integral" \<rightleftharpoons> set_lebesgue_integral
 translations
-"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
-
-translations
-"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
+  "LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
+  "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
 
 lemma set_integral_reflect:
   fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
diff -r 10e3a30b2512 -r f270cd6ee185 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Fri Oct 18 14:35:13 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Oct 18 14:37:09 2024 +0200
@@ -30,22 +30,6 @@
 translations
   "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
 
-(*
-    Notation for integration wrt lebesgue measure on the reals:
-
-      LBINT x. f
-      LBINT x : A. f
-
-    TODO: keep all these? Need unicode.
-*)
-
-syntax
-  "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(\<open>indent=2 notation=\<open>binder LBINT\<close>\<close>LBINT _./ _)\<close> [0,10] 10)
-
-syntax
-  "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(\<open>indent=3 notation=\<open>binder LBINT\<close>\<close>LBINT _:_./ _)\<close> [0,0,10] 10)
 
 section \<open>Basic properties\<close>