src/HOL/NthRoot.thy
changeset 44289 d81d09cdab9c
parent 35216 7641e8d831d2
child 44320 33439faadd67
     1.1 --- a/src/HOL/NthRoot.thy	Thu Aug 18 18:10:23 2011 -0700
     1.2 +++ b/src/HOL/NthRoot.thy	Thu Aug 18 19:53:03 2011 -0700
     1.3 @@ -29,7 +29,7 @@
     1.4        using n1 by (rule power_increasing, simp)
     1.5      finally show "a \<le> max 1 a ^ n" .
     1.6      show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
     1.7 -      by (simp add: isCont_power)
     1.8 +      by simp
     1.9    qed
    1.10    then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
    1.11    with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
    1.12 @@ -310,7 +310,7 @@
    1.13      show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
    1.14        by (simp add: abs_le_iff real_root_power_cancel n)
    1.15      show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
    1.16 -      by (simp add: isCont_power)
    1.17 +      by simp
    1.18    qed
    1.19    thus ?thesis using n x by simp
    1.20  qed
    1.21 @@ -320,7 +320,7 @@
    1.22  apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
    1.23  apply (simp add: real_root_minus)
    1.24  apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
    1.25 -apply (simp add: isCont_minus isCont_root_pos)
    1.26 +apply (simp add: isCont_root_pos)
    1.27  done
    1.28  
    1.29  lemma isCont_root_zero: