src/HOL/Hyperreal/HTranscendental.thy
changeset 23096 423ad2fe9f76
parent 22983 3314057c3b57
child 23114 1bd84606b403
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Thu May 24 16:52:54 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu May 24 22:55:53 2007 +0200
     1.3 @@ -87,14 +87,14 @@
     1.4       "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
     1.5  apply (rule hypreal_sqrt_approx_zero2)
     1.6  apply (rule add_nonneg_nonneg)+
     1.7 -apply (auto simp add: zero_le_square)
     1.8 +apply (auto)
     1.9  done
    1.10  
    1.11  lemma hypreal_sqrt_sum_squares2 [simp]:
    1.12       "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
    1.13  apply (rule hypreal_sqrt_approx_zero2)
    1.14  apply (rule add_nonneg_nonneg)
    1.15 -apply (auto simp add: zero_le_square)
    1.16 +apply (auto)
    1.17  done
    1.18  
    1.19  lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
    1.20 @@ -157,7 +157,7 @@
    1.21       "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
    1.22  apply (rule HFinite_hypreal_sqrt_iff)
    1.23  apply (rule add_nonneg_nonneg)
    1.24 -apply (auto simp add: zero_le_square)
    1.25 +apply (auto)
    1.26  done
    1.27  
    1.28  lemma Infinitesimal_hypreal_sqrt:
    1.29 @@ -184,7 +184,7 @@
    1.30       "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
    1.31  apply (rule Infinitesimal_hypreal_sqrt_iff)
    1.32  apply (rule add_nonneg_nonneg)
    1.33 -apply (auto simp add: zero_le_square)
    1.34 +apply (auto)
    1.35  done
    1.36  
    1.37  lemma HInfinite_hypreal_sqrt:
    1.38 @@ -211,7 +211,7 @@
    1.39       "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
    1.40  apply (rule HInfinite_hypreal_sqrt_iff)
    1.41  apply (rule add_nonneg_nonneg)
    1.42 -apply (auto simp add: zero_le_square)
    1.43 +apply (auto)
    1.44  done
    1.45  
    1.46  lemma HFinite_exp [simp]: