src/HOL/Hyperreal/HTranscendental.thy

 
 lemma hypreal_sqrt_sum_squares [simp]:
      "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
 apply (rule hypreal_sqrt_approx_zero2)
 apply (rule add_nonneg_nonneg)+
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma hypreal_sqrt_sum_squares2 [simp]:
      "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
 apply (rule hypreal_sqrt_approx_zero2)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
 apply transfer
 apply (auto intro: real_sqrt_gt_zero)

 
 lemma HFinite_sqrt_sum_squares [simp]:
      "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
 apply (rule HFinite_hypreal_sqrt_iff)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma Infinitesimal_hypreal_sqrt:
      "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
 apply (auto simp add: order_le_less)

 
 lemma Infinitesimal_sqrt_sum_squares [simp]:
      "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
 apply (rule Infinitesimal_hypreal_sqrt_iff)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma HInfinite_hypreal_sqrt:
      "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
 apply (auto simp add: order_le_less)

 
 lemma HInfinite_sqrt_sum_squares [simp]:
      "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
 apply (rule HInfinite_hypreal_sqrt_iff)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma HFinite_exp [simp]:
      "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
 unfolding sumhr_app