# HG changeset patch
# User huffman
# Date 1313790405 25200
# Node ID 471ff02a85741c75ea62863f0dc74429db301c9f
# Parent  42c5cbf680520c4cc3254ff953f9672fb5463c5b
delete unused lemmas about limits

diff -r 42c5cbf68052 -r 471ff02a8574 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Fri Aug 19 14:17:28 2011 -0700
+++ b/src/HOL/Lim.thy	Fri Aug 19 14:46:45 2011 -0700
@@ -102,12 +102,6 @@
   shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
 by (rule tendsto_minus)
 
-(* TODO: delete *)
-lemma LIM_add_minus:
-  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
-  shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
-by (intro LIM_add LIM_minus)
-
 lemma LIM_diff:
   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
@@ -235,14 +229,6 @@
   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
 
-text{*Two uses in Transcendental.ML*} (* BH: no longer true; delete? *)
-lemma LIM_trans:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
-apply (drule LIM_add, assumption)
-apply (auto simp add: add_assoc)
-done
-
 lemma LIM_compose:
   assumes g: "g -- l --> g l"
   assumes f: "f -- a --> l"