changeset 31404 | 05d2eddc5d41 |
parent 31338 | d41a8ba25b67 |
child 31880 | 6fb86c61747c |
--- 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