src/HOL/Lim.thy
 changeset 44312 471ff02a8574 parent 44310 ba3d031b5dbb child 44314 dbad46932536
```     1.1 --- a/src/HOL/Lim.thy	Fri Aug 19 14:17:28 2011 -0700
1.2 +++ b/src/HOL/Lim.thy	Fri Aug 19 14:46:45 2011 -0700
1.3 @@ -102,12 +102,6 @@
1.4    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
1.5  by (rule tendsto_minus)
1.6
1.7 -(* TODO: delete *)
1.9 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.10 -  shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
1.12 -
1.13  lemma LIM_diff:
1.14    fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.15    shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
1.16 @@ -235,14 +229,6 @@
1.17    shows "g -- a --> l \<Longrightarrow> f -- a --> l"
1.18  by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
1.19
1.20 -text{*Two uses in Transcendental.ML*} (* BH: no longer true; delete? *)
1.21 -lemma LIM_trans:
1.22 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.23 -  shows "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"