Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Complete_Lattices.thy
changeset 81125 ec121999a9cb
parent 80934 8e72f55295fd 
--- a/src/HOL/Complete_Lattices.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Complete_Lattices.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -15,10 +15,10 @@
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
-  fixes Inf :: "'a set \<Rightarrow> 'a"  (\<open>\<Sqinter> _\<close> [900] 900)
+  fixes Inf :: "'a set \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>prefix \<Sqinter>\<close>\<close>\<Sqinter> _)\<close> [900] 900)
 
 class Sup =
-  fixes Sup :: "'a set \<Rightarrow> 'a"  (\<open>\<Squnion> _\<close> [900] 900)
+  fixes Sup :: "'a set \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>prefix \<Squnion>\<close>\<close>\<Squnion> _)\<close> [900] 900)
 
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder INF\<close>\<close>INF _./ _)\<close> [0, 10] 10)
isabelle