haftmann@30330: (* Author: Florian Haftmann, TU Muenchen *)
haftmann@30330: 
haftmann@30330: header {* Pretty syntax for lattice operations *}
haftmann@30330: 
haftmann@30330: theory Lattice_Syntax
haftmann@44860: imports Complete_Lattices
haftmann@30330: begin
haftmann@30330: 
haftmann@30330: notation
haftmann@41082:   bot ("\<bottom>") and
haftmann@32139:   top ("\<top>") and
haftmann@30330:   inf  (infixl "\<sqinter>" 70) and
haftmann@30330:   sup  (infixl "\<squnion>" 65) and
haftmann@30330:   Inf  ("\<Sqinter>_" [900] 900) and
haftmann@32139:   Sup  ("\<Squnion>_" [900] 900)
haftmann@30330: 
haftmann@41080: syntax (xsymbols)
haftmann@41082:   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
haftmann@41082:   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
haftmann@41080:   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
haftmann@41080:   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
haftmann@41080: 
haftmann@30331: end