diff -r 4d15005da582 -r 5b1f86d8505c src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Thu Jan 09 13:18:37 2025 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Jan 10 15:11:56 2025 +0000
@@ -45,19 +45,19 @@
   "{l..} == {x. l\<le>x}"
 
 definition
-  greaterThanLessThan :: "'a => 'a => 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..<_})\<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>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..<_})\<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>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<.._})\<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>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_.._})\<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