src/HOL/Limits.thy
 changeset 44079 bcc60791b7b9 parent 41970 47d6e13d1710 child 44081 730f7cced3a6
```     1.1 --- a/src/HOL/Limits.thy	Mon Aug 08 16:19:57 2011 -0700
1.2 +++ b/src/HOL/Limits.thy	Mon Aug 08 16:57:37 2011 -0700
1.3 @@ -644,16 +644,6 @@
1.4    "((\<lambda>x. norm (f x)) ---> 0) net \<longleftrightarrow> (f ---> 0) net"
1.5  unfolding tendsto_iff dist_norm by simp
1.6
1.8 -  fixes a b c d :: "'a::ab_group_add"
1.9 -  shows "(a + c) - (b + d) = (a - b) + (c - d)"
1.10 -by simp
1.11 -
1.12 -lemma minus_diff_minus:
1.13 -  fixes a b :: "'a::ab_group_add"
1.14 -  shows "(- a) - (- b) = - (a - b)"
1.15 -by simp
1.16 -
1.18    fixes a b :: "'a::real_normed_vector"
1.19    shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net"
1.20 @@ -748,11 +738,6 @@
1.21    shows "Zfun (\<lambda>x. f x ** g x) net"
1.22  using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
1.23
1.24 -lemma inverse_diff_inverse:
1.25 -  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
1.26 -   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"