Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more uniform syntax;
authorwenzelm
Tue, 21 Sep 2021 11:34:58 +0200
changeset 74337 9c1ad2f04660
parent 74336 7bb0ac635397
child 74338 534b231ce041
more uniform syntax;
src/HOL/Complete_Lattices.thy file | annotate | diff | comparison | revisions
src/HOL/Main.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle