--- 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)\<twosuperior>" 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)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2 |]
==> (sin xa)\<twosuperior> = (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)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]
==> (cos xa)\<twosuperior> = (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\<twosuperior>" in real_sum_of_halves [THEN subst])
apply (rule add_mono)