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>