# HG changeset patch
# User huffman
# Date 1180046214 -7200
# Node ID f4779adcd1a2702b5e2c9ddcbb16e9328c2f1721
# Parent  423ad2fe9f7662ea2272339b6a2443c07a0c032f
simplify some proofs

diff -r 423ad2fe9f76 -r f4779adcd1a2 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Thu May 24 22:55:53 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri May 25 00:36:54 2007 +0200
@@ -1027,12 +1027,7 @@
 by arith
 
 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
-apply (auto simp add: linorder_not_less [symmetric])
-apply (drule_tac n = "Suc 0" in power_gt1)
-apply (auto simp del: realpow_Suc)
-apply (drule_tac r1 = "cos x" in realpow_two_le [THEN [2] real_gt_one_ge_zero_add_less])
-apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
-done
+by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
 
 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
 apply (insert abs_sin_le_one [of x]) 
@@ -1045,12 +1040,7 @@
 done
 
 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
-apply (auto simp add: linorder_not_less [symmetric])
-apply (drule_tac n = "Suc 0" in power_gt1)
-apply (auto simp del: realpow_Suc)
-apply (drule_tac r1 = "sin x" in realpow_two_le [THEN [2] real_gt_one_ge_zero_add_less])
-apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
-done
+by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
 
 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
 apply (insert abs_cos_le_one [of x])