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/Algebra/Lattice.thy
changeset 81142 6ad2c917dd2e
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Algebra/Lattice.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -15,11 +15,11 @@
 subsection \<open>Supremum and infimum\<close>
 
 definition
-  sup :: "[_, 'a set] => 'a" (\<open>\<Squnion>\<index>_\<close> [90] 90)
+  sup :: "[_, 'a set] => 'a" (\<open>(\<open>open_block notation=\<open>prefix \<Squnion>\<close>\<close>\<Squnion>\<index>_)\<close> [90] 90)
   where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
 
 definition
-  inf :: "[_, 'a set] => 'a" (\<open>\<Sqinter>\<index>_\<close> [90] 90)
+  inf :: "[_, 'a set] => 'a" (\<open>(\<open>open_block notation=\<open>prefix \<Sqinter>\<close>\<close>\<Sqinter>\<index>_)\<close> [90] 90)
   where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
 
 definition supr :: 
@@ -31,15 +31,17 @@
   where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
 
 syntax
-  "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3IINF\<index> _./ _)\<close> [0, 10] 10)
-  "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3IINF\<index> _:_./ _)\<close> [0, 0, 10] 10)
-  "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3SSUP\<index> _./ _)\<close> [0, 10] 10)
-  "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3SSUP\<index> _:_./ _)\<close> [0, 0, 10] 10)
-
+  "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder IINF\<close>\<close>IINF\<index> _./ _)\<close> [0, 10] 10)
+  "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder IINF\<close>\<close>IINF\<index> _:_./ _)\<close> [0, 0, 10] 10)
+  "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder SSUP\<close>\<close>SSUP\<index> _./ _)\<close> [0, 10] 10)
+  "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder SSUP\<close>\<close>SSUP\<index> _:_./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_inf1" "_inf" == infi and
   "_sup1" "_sup" == supr
-
 translations
   "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
   "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
isabelle