src/HOL/Hyperreal/Transcendental.thy

        in lemma_termdiff5)
 apply (auto simp add: add_commute)
 apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
 apply (rule_tac [2] x = K in powser_insidea, auto)
 apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
-apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eq], auto)
+apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
 apply (simp add: diffs_def mult_assoc [symmetric])
 apply (subgoal_tac
         "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
               = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
 apply auto

 apply (blast intro: polar_ex1 polar_ex2)+
 done
 
 lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
 apply (rule_tac n = 1 in realpow_increasing)
-apply (auto simp add: numeral_2_eq_2 [symmetric])
+apply (auto simp add: numeral_2_eq_2 [symmetric] power2_abs)
 done
 
 lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
 apply (rule real_add_commute [THEN subst])
 apply (rule real_sqrt_ge_abs1)

 apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
 apply (rule add_mono)
 apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
 done
 
-declare real_sqrt_sum_squares_ge_zero [THEN abs_eq, simp]
+declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
 
 
 subsection{*A Few Theorems Involving Ln, Derivatives, etc.*}
 
 lemma lemma_DERIV_ln: