equal
deleted
inserted
replaced
564 apply (case_tac "r=0") |
564 apply (case_tac "r=0") |
565 apply (auto simp add: mult_ac) |
565 apply (auto simp add: mult_ac) |
566 done |
566 done |
567 |
567 |
568 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" |
568 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" |
569 by (simp add: divide_less_eq mult_compare_simps) |
569 by (simp add: divide_less_eq) |
570 |
570 |
571 lemma four_x_squared: |
571 lemma four_x_squared: |
572 fixes x::real |
572 fixes x::real |
573 shows "4 * x\<twosuperior> = (2 * x)\<twosuperior>" |
573 shows "4 * x\<twosuperior> = (2 * x)\<twosuperior>" |
574 by (simp add: power2_eq_square) |
574 by (simp add: power2_eq_square) |