delete unused lemmas about limits
authorhuffman
Fri Aug 19 14:46:45 2011 -0700 (2011-08-19)
changeset 44312471ff02a8574
parent 44311 42c5cbf68052
child 44313 d81d57979771
delete unused lemmas about limits
src/HOL/Lim.thy
     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.8 -lemma LIM_add_minus:
     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.11 -by (intro LIM_add LIM_minus)
    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"
    1.24 -apply (drule LIM_add, assumption)
    1.25 -apply (auto simp add: add_assoc)
    1.26 -done
    1.27 -
    1.28  lemma LIM_compose:
    1.29    assumes g: "g -- l --> g l"
    1.30    assumes f: "f -- a --> l"