equal
deleted
inserted
replaced
13 and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x" |
13 and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x" |
14 |
14 |
15 lemmas [elim?] = lub.least lub.upper |
15 lemmas [elim?] = lub.least lub.upper |
16 |
16 |
17 definition |
17 definition |
18 the_lub :: "'a::order set \<Rightarrow> 'a" |
18 the_lub :: "'a::order set \<Rightarrow> 'a" where |
19 "the_lub A = The (lub A)" |
19 "the_lub A = The (lub A)" |
20 |
20 |
21 notation (xsymbols) |
21 notation (xsymbols) |
22 the_lub ("\<Squnion>_" [90] 90) |
22 the_lub ("\<Squnion>_" [90] 90) |
23 |
23 |