src/HOL/Deriv.thy

--- a/src/HOL/Deriv.thy	Tue Jun 02 23:06:05 2009 -0700
+++ b/src/HOL/Deriv.thy	Tue Jun 02 23:31:03 2009 -0700
@@ -457,7 +457,9 @@
 apply (auto intro: order_trans simp add: diff_minus abs_if)
 done
 
-lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)"
+lemma lim_uminus:
+  fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "convergent g ==> lim (%x. - g x) = - (lim g)"
 apply (rule LIMSEQ_minus [THEN limI])
 apply (simp add: convergent_LIMSEQ_iff)
 done