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