# HG changeset patch
# User wenzelm
# Date 1632216898 -7200
# Node ID 9c1ad2f04660add6a8c016b3e0f03278f18c94ed
# Parent  7bb0ac635397c20d0927c283aaed51f4ffe1aa14
more uniform syntax;

diff -r 7bb0ac635397 -r 9c1ad2f04660 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Sep 21 11:23:18 2021 +0200
+++ b/src/HOL/Complete_Lattices.thy	Tue Sep 21 11:34:58 2021 +0200
@@ -15,10 +15,10 @@
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
-  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>")
+  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter> _" [900] 900)
 
 class Sup =
-  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>")
+  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion> _" [900] 900)
 
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
diff -r 7bb0ac635397 -r 9c1ad2f04660 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Sep 21 11:23:18 2021 +0200
+++ b/src/HOL/Main.thy	Tue Sep 21 11:34:58 2021 +0200
@@ -104,6 +104,5 @@
 end
 
 unbundle no_lattice_syntax
-no_notation Inf ("\<Sqinter>") and Sup ("\<Squnion>")
 
 end