src/HOL/NthRoot.thy
changeset 61649 268d88ec9087
parent 61609 77b453bd616f
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/NthRoot.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -257,7 +257,7 @@
     1.4    have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
     1.5      using n by (intro continuous_on_If continuous_intros) auto
     1.6    then have "continuous_on UNIV ?f"
     1.7 -    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
     1.8 +    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less sgn_neg le_less n)
     1.9    then have [simp]: "\<And>x. isCont ?f x"
    1.10      by (simp add: continuous_on_eq_continuous_at)
    1.11  
    1.12 @@ -697,7 +697,7 @@
    1.13             (simp_all add: at_infinity_eq_at_top_bot)
    1.14        { fix n :: nat assume "1 < n"
    1.15          have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
    1.16 -          using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp 
    1.17 +          using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp
    1.18          also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
    1.19            by (simp add: x_def)
    1.20          also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    1.21 @@ -741,8 +741,4 @@
    1.22  lemmas real_sqrt_mult_distrib2 = real_sqrt_mult
    1.23  lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff
    1.24  
    1.25 -(* needed for CauchysMeanTheorem.het_base from AFP *)
    1.26 -lemma real_root_pos: "0 < x \<Longrightarrow> root (Suc n) (x ^ (Suc n)) = x"
    1.27 -by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le])
    1.28 -
    1.29  end