equal
deleted
inserted
replaced
14 axclass |
14 axclass |
15 clattice < order |
15 clattice < order |
16 ex_Inf "ALL A. EX inf. is_Inf A inf" |
16 ex_Inf "ALL A. EX inf. is_Inf A inf" |
17 ex_Sup "ALL A. EX sup. is_Sup A sup" |
17 ex_Sup "ALL A. EX sup. is_Sup A sup" |
18 |
18 |
19 consts |
19 constdefs |
20 Inf :: "'a::clattice set => 'a" |
20 Inf :: "'a::clattice set => 'a" |
|
21 "Inf A == @inf. is_Inf A inf" |
|
22 |
21 Sup :: "'a::clattice set => 'a" |
23 Sup :: "'a::clattice set => 'a" |
22 |
24 "Sup A == @sup. is_Sup A sup" |
23 defs |
|
24 Inf_def "Inf A == @inf. is_Inf A inf" |
|
25 Sup_def "Sup A == @sup. is_Sup A sup" |
|
26 |
25 |
27 end |
26 end |