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")