header {* Pretty syntax for lattice operations *}
theory Lattice_Syntax
imports Complete_Lattices
begin
notation
bot ("⊥") and
top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
Sup ("\<Squnion>_" [900] 900)
syntax (xsymbols)
"_INF1" :: "pttrns => 'b => 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
"_INF" :: "pttrn => 'a set => 'b => 'b" ("(3\<Sqinter>_∈_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns => 'b => 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
"_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3\<Squnion>_∈_./ _)" [0, 0, 10] 10)
end