src/HOL/Multivariate_Analysis/Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Mar 03 18:43:15 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Mar 03 21:43:06 2011 +0100
@@ -644,7 +644,7 @@
 
 lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m"
   shows "\<forall>n \<ge> m. d n < e m"
-  using prems apply auto
+  using assms apply auto
   apply (erule_tac x="n" in allE)
   apply (erule_tac x="n" in allE)
   apply auto