equal
deleted
inserted
replaced
25 *} |
25 *} |
26 |
26 |
27 consts |
27 consts |
28 meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "&&" 70) |
28 meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "&&" 70) |
29 join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65) |
29 join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65) |
30 syntax (symbols) |
30 syntax (xsymbols) |
31 meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
31 meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
32 join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
32 join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
33 defs |
33 defs |
34 meet_def: "x && y \<equiv> THE inf. is_inf x y inf" |
34 meet_def: "x && y \<equiv> THE inf. is_inf x y inf" |
35 join_def: "x || y \<equiv> THE sup. is_sup x y sup" |
35 join_def: "x || y \<equiv> THE sup. is_sup x y sup" |