# HG changeset patch # User huffman # Date 1158073432 -7200 # Node ID 2d2e1d323a0594cc33c539d9dfee362999b88d8f # Parent 3ef9eb57d769e7b92d2062bfac0e51c3df7e74e3 realpow_divide -> power_divide diff -r 3ef9eb57d769 -r 2d2e1d323a05 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Tue Sep 12 16:44:04 2006 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Tue Sep 12 17:03:52 2006 +0200 @@ -1971,7 +1971,7 @@ apply (rule power_inverse [THEN subst]) apply (rule_tac c1 = "(cos x)\" in real_mult_right_cancel [THEN iffD1]) apply (auto dest: realpow_not_zero - simp add: power_mult_distrib left_distrib realpow_divide tan_def + simp add: power_mult_distrib left_distrib power_divide tan_def mult_assoc power_inverse [symmetric] simp del: realpow_Suc) done @@ -2314,14 +2314,14 @@ 1 - (sin xa)\ = (x / sqrt (x * x + y * y)) ^ 2 |] ==> (sin xa)\ = (y / sqrt (x * x + y * y)) ^ 2" by (auto intro: lemma_divide_rearrange - simp add: realpow_divide power2_eq_square [symmetric]) + simp add: power_divide power2_eq_square [symmetric]) lemma lemma_sin_cos_eq: "[| 0 < x * x + y * y; 1 - (cos xa)\ = (y / sqrt (x * x + y * y)) ^ 2 |] ==> (cos xa)\ = (x / sqrt (x * x + y * y)) ^ 2" -apply (auto simp add: realpow_divide power2_eq_square [symmetric]) +apply (auto simp add: power_divide power2_eq_square [symmetric]) apply (subst add_commute) apply (rule lemma_divide_rearrange, simp add: real_add_eq_0_iff) apply (simp add: add_commute) @@ -2459,7 +2459,7 @@ apply (rule_tac y = "u/sqrt 2" in order_le_less_trans) apply (erule_tac [2] lemma_real_divide_sqrt_less) apply (rule_tac n = 1 in realpow_increasing) -apply (auto simp add: real_0_le_divide_iff realpow_divide numeral_2_eq_2 [symmetric] +apply (auto simp add: real_0_le_divide_iff power_divide numeral_2_eq_2 [symmetric] simp del: realpow_Suc) apply (rule_tac t = "u\" in real_sum_of_halves [THEN subst]) apply (rule add_mono)