# HG changeset patch
# User huffman
# Date 1244010663 25200
# Node ID 05d2eddc5d4173b6140d8429b0053ace85f24d11
# Parent  0baaad47cef21aca392d94e6e48269fff69aa2db
generalize type of constant lim

diff -r 0baaad47cef2 -r 05d2eddc5d41 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
diff -r 0baaad47cef2 -r 05d2eddc5d41 src/HOL/SEQ.thy
--- 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)"