bot comes before top, inf before sup etc.
1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* Pretty syntax for lattice operations *}
6 imports Complete_Lattice
12 inf (infixl "\<sqinter>" 70) and
13 sup (infixl "\<squnion>" 65) and
14 Inf ("\<Sqinter>_" [900] 900) and
15 Sup ("\<Squnion>_" [900] 900)
18 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
19 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
20 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
21 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)