src/HOL/Lim.thy

--- a/src/HOL/Lim.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Lim.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -386,7 +386,7 @@
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
   assumes f: "f -- a --> l"
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
-by (induct n, simp, simp add: power_Suc LIM_mult f)
+by (induct n, simp, simp add: LIM_mult f)
 
 subsubsection {* Derived theorems about @{term LIM} *}