equal
deleted
inserted
replaced
22 lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semidom)" |
22 lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semidom)" |
23 by (insert add_strict_mono [of 0 a b c], simp) |
23 by (insert add_strict_mono [of 0 a b c], simp) |
24 |
24 |
25 lemma interval_empty_iff: |
25 lemma interval_empty_iff: |
26 "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))" |
26 "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))" |
27 by (blast dest: dense intro: order_less_trans) |
27 by (auto dest: dense) |
28 |
28 |
29 |
29 |
30 constdefs |
30 constdefs |
31 cut :: "rat set => bool" |
31 cut :: "rat set => bool" |
32 "cut A == {} \<subset> A & |
32 "cut A == {} \<subset> A & |