diff -r fe9c2398c330 -r d81d09cdab9c src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Thu Aug 18 18:10:23 2011 -0700
+++ b/src/HOL/NthRoot.thy	Thu Aug 18 19:53:03 2011 -0700
@@ -29,7 +29,7 @@
       using n1 by (rule power_increasing, simp)
     finally show "a \<le> max 1 a ^ n" .
     show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
-      by (simp add: isCont_power)
+      by simp
   qed
   then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
   with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
@@ -310,7 +310,7 @@
     show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
       by (simp add: abs_le_iff real_root_power_cancel n)
     show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
-      by (simp add: isCont_power)
+      by simp
   qed
   thus ?thesis using n x by simp
 qed
@@ -320,7 +320,7 @@
 apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
 apply (simp add: real_root_minus)
 apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
-apply (simp add: isCont_minus isCont_root_pos)
+apply (simp add: isCont_root_pos)
 done
 
 lemma isCont_root_zero: