--- 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)
--- 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