diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -29,35 +29,35 @@
 begin
 
 definition
-  lessThan    :: "'a => 'a set" (\<open>(1{..<_})\<close>) where
+  lessThan    :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{..<_})\<close>) where
   "{..<u} == {x. x < u}"
 
 definition
-  atMost      :: "'a => 'a set" (\<open>(1{.._})\<close>) where
+  atMost      :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{.._})\<close>) where
   "{..u} == {x. x \<le> u}"
 
 definition
-  greaterThan :: "'a => 'a set" (\<open>(1{_<..})\<close>) where
+  greaterThan :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..})\<close>) where
   "{l<..} == {x. l<x}"
 
 definition
-  atLeast     :: "'a => 'a set" (\<open>(1{_..})\<close>) where
+  atLeast     :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..})\<close>) where
   "{l..} == {x. l\<le>x}"
 
 definition
-  greaterThanLessThan :: "'a => 'a => 'a set"  (\<open>(1{_<..<_})\<close>) where
+  greaterThanLessThan :: "'a => 'a => 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..<_})\<close>) where
   "{l<..<u} == {l<..} Int {..<u}"
 
 definition
-  atLeastLessThan :: "'a => 'a => 'a set"      (\<open>(1{_..<_})\<close>) where
+  atLeastLessThan :: "'a => 'a => 'a set"      (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..<_})\<close>) where
   "{l..<u} == {l..} Int {..<u}"
 
 definition
-  greaterThanAtMost :: "'a => 'a => 'a set"    (\<open>(1{_<.._})\<close>) where
+  greaterThanAtMost :: "'a => 'a => 'a set"    (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<.._})\<close>) where
   "{l<..u} == {l<..} Int {..u}"
 
 definition
-  atLeastAtMost :: "'a => 'a => 'a set"        (\<open>(1{_.._})\<close>) where
+  atLeastAtMost :: "'a => 'a => 'a set"        (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_.._})\<close>) where
   "{l..u} == {l..} Int {..u}"
 
 end
@@ -67,10 +67,10 @@
 \<^term>\<open>{m..<n}\<close> may not exist in \<^term>\<open>{..<n}\<close>-form as well.\<close>
 
 syntax (ASCII)
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3UN _<=_./ _)\<close> [0, 0, 10] 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3UN _<_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3INT _<=_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3INT _<_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<=_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<=_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<_./ _)\<close> [0, 0, 10] 10)
 
 syntax (latex output)
   "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       (\<open>(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
@@ -79,10 +79,10 @@
   "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       (\<open>(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Union>_<_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_<_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
@@ -1988,10 +1988,10 @@
 subsection \<open>Summation indexed over intervals\<close>
 
 syntax (ASCII)
-  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _<_./ _)\<close> [0,0,10] 10)
-  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _<=_./ _)\<close> [0,0,10] 10)
+  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<_./ _)\<close> [0,0,10] 10)
+  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<=_./ _)\<close> [0,0,10] 10)
 
 syntax (latex_sum output)
   "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2004,10 +2004,10 @@
  (\<open>(3\<^latex>\<open>$\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
 
 syntax
-  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_<_./ _)\<close> [0,0,10] 10)
-  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
+  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_<_./ _)\<close> [0,0,10] 10)
+  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
 
 syntax_consts
   "_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
@@ -2681,10 +2681,10 @@
 subsection \<open>Products indexed over intervals\<close>
 
 syntax (ASCII)
-  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _<_./ _)\<close> [0,0,10] 10)
-  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _<=_./ _)\<close> [0,0,10] 10)
+  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<_./ _)\<close> [0,0,10] 10)
+  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<=_./ _)\<close> [0,0,10] 10)
 
 syntax (latex_prod output)
   "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2697,10 +2697,10 @@
  (\<open>(3\<^latex>\<open>$\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
 
 syntax
-  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_<_./ _)\<close> [0,0,10] 10)
-  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
+  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_<_./ _)\<close> [0,0,10] 10)
+  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
 
 syntax_consts
   "_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod