src/HOL/NSA/HSEQ.thy

--- a/src/HOL/NSA/HSEQ.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/NSA/HSEQ.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -110,7 +110,7 @@
 done
 
 lemma NSLIMSEQ_pow [rule_format]:
-  fixes a :: "'a::{real_normed_algebra,recpower}"
+  fixes a :: "'a::{real_normed_algebra,power}"
   shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
 apply (induct "m")
 apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)