--- 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
--- a/src/HOL/SEQ.thy Tue Jun 02 23:06:05 2009 -0700
+++ b/src/HOL/SEQ.thy Tue Jun 02 23:31:03 2009 -0700
@@ -24,7 +24,7 @@
[code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
definition
- lim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where
+ lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
--{*Standard definition of limit using choice operator*}
"lim X = (THE L. X ----> L)"