diff -r d164c4fc0d2c -r f533820e7248 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/NthRoot.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Nth Roots of Real Numbers\<close>
 
 theory NthRoot
-  imports Deriv Binomial
+  imports Deriv
 begin
 
 
@@ -469,7 +469,7 @@
 lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
   using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
 
-lemma real_sqrt_power_even: 
+lemma real_sqrt_power_even:
   assumes "even n" "x \<ge> 0"
   shows   "sqrt x ^ n = x ^ (n div 2)"
 proof -