equal
deleted
inserted
replaced
32 *} |
32 *} |
33 |
33 |
34 consts |
34 consts |
35 Meet :: "'a::complete_lattice set \<Rightarrow> 'a" |
35 Meet :: "'a::complete_lattice set \<Rightarrow> 'a" |
36 Join :: "'a::complete_lattice set \<Rightarrow> 'a" |
36 Join :: "'a::complete_lattice set \<Rightarrow> 'a" |
37 syntax (symbols) |
37 syntax (xsymbols) |
38 Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90) |
38 Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90) |
39 Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90) |
39 Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90) |
40 defs |
40 defs |
41 Meet_def: "\<Sqinter>A \<equiv> THE inf. is_Inf A inf" |
41 Meet_def: "\<Sqinter>A \<equiv> THE inf. is_Inf A inf" |
42 Join_def: "\<Squnion>A \<equiv> THE sup. is_Sup A sup" |
42 Join_def: "\<Squnion>A \<equiv> THE sup. is_Sup A sup" |