equal
deleted
inserted
replaced
16 |
16 |
17 definition |
17 definition |
18 the_lub :: "'a::order set \<Rightarrow> 'a" |
18 the_lub :: "'a::order set \<Rightarrow> 'a" |
19 "the_lub A = The (lub A)" |
19 "the_lub A = The (lub A)" |
20 |
20 |
21 const_syntax (xsymbols) |
21 notation (xsymbols) |
22 the_lub ("\<Squnion>_" [90] 90) |
22 the_lub ("\<Squnion>_" [90] 90) |
23 |
23 |
24 lemma the_lub_equality [elim?]: |
24 lemma the_lub_equality [elim?]: |
25 includes lub |
25 includes lub |
26 shows "\<Squnion>A = (x::'a::order)" |
26 shows "\<Squnion>A = (x::'a::order)" |