equal
deleted
inserted
replaced
221 |
221 |
222 lemma minus1_divide [simp]: |
222 lemma minus1_divide [simp]: |
223 "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" |
223 "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" |
224 by (simp add: divide_inverse inverse_minus_eq) |
224 by (simp add: divide_inverse inverse_minus_eq) |
225 |
225 |
|
226 lemma half_gt_zero_iff: |
|
227 "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" |
|
228 by auto |
|
229 |
|
230 lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp] |
|
231 |
226 |
232 |
227 |
233 |
228 |
234 |
229 ML |
235 ML |
230 {* |
236 {* |