# HG changeset patch
# User huffman
# Date 1176047692 -7200
# Node ID 2f119f54d1500bfc269b7de461a3d5e1b18ff490
# Parent  1f017e6a0395361c821cdce868bdaeebc7c830dc
remove redundant lemmas

diff -r 1f017e6a0395 -r 2f119f54d150 src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Sat Apr 07 18:54:30 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Sun Apr 08 17:54:52 2007 +0200
@@ -122,7 +122,7 @@
   hence "(\<lambda>h. f(x+h) * ((g(x+h) - g x) / h) +
               ((f(x+h) - f x) / h) * g x)
           -- 0 --> f x * E + D * g x"
-    by (intro LIM_add LIM_mult2 LIM_const DERIV_D f g)
+    by (intro LIM_add LIM_mult LIM_const DERIV_D f g)
   thus "(\<lambda>h. (f(x+h) * g(x+h) - f x * g x) / h)
          -- 0 --> f x * E + D * g x"
     by (simp only: DERIV_mult_lemma)
@@ -204,7 +204,7 @@
       by (unfold DERIV_iff2)
     thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x)))
           -- x --> ?E"
-      by (intro LIM_mult2 LIM_inverse LIM_minus LIM_const lim_f neq)
+      by (intro LIM_mult LIM_inverse LIM_minus LIM_const lim_f neq)
   qed
 qed
 
diff -r 1f017e6a0395 -r 2f119f54d150 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Sat Apr 07 18:54:30 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sun Apr 08 17:54:52 2007 +0200
@@ -557,52 +557,12 @@
 
 subsubsection {* Derived theorems about @{term LIM} *}
 
-lemma LIM_mult2:
-  fixes l m :: "'a::real_normed_algebra"
-  shows "[| f -- x --> l; g -- x --> m |]
-      ==> (%x. f(x) * g(x)) -- x --> (l * m)"
-by (simp add: LIM_NSLIM_iff NSLIM_mult)
-
-lemma LIM_scaleR:
-  "[| f -- x --> l; g -- x --> m |]
-      ==> (%x. f(x) *# g(x)) -- x --> (l *# m)"
-by (simp add: LIM_NSLIM_iff NSLIM_scaleR)
-
-lemma LIM_add2:
-     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
-by (simp add: LIM_NSLIM_iff NSLIM_add)
-
-lemma LIM_const2: "(%x. k) -- x --> k"
-by (simp add: LIM_NSLIM_iff)
-
-lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
-by (simp add: LIM_NSLIM_iff NSLIM_minus)
-
-lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
-by (simp add: LIM_NSLIM_iff NSLIM_add_minus)
-
 lemma LIM_inverse:
   fixes L :: "'a::real_normed_div_algebra"
   shows "[| f -- a --> L; L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --> (inverse L)"
 by (simp add: LIM_NSLIM_iff NSLIM_inverse)
 
-lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) - l) -- a --> 0"
-by (simp add: LIM_NSLIM_iff NSLIM_zero)
-
-lemma LIM_unique2:
-  fixes a :: real
-  shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
-by (simp add: LIM_NSLIM_iff NSLIM_unique)
-
-(* we can use the corresponding thm LIM_mult2 *)
-(* for standard definition of limit           *)
-
-lemma LIM_mult_zero2:
-  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
-by (drule LIM_mult2, auto)
-
 
 subsection {* Continuity *}
 
diff -r 1f017e6a0395 -r 2f119f54d150 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sat Apr 07 18:54:30 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun Apr 08 17:54:52 2007 +0200
@@ -1628,7 +1628,7 @@
 lemma LIM_cos_div_sin [simp]: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
 apply (subgoal_tac "(\<lambda>x. cos x * inverse (sin x)) -- pi * inverse 2 --> 0*1")
 apply (simp add: divide_inverse [symmetric])
-apply (rule LIM_mult2)
+apply (rule LIM_mult)
 apply (rule_tac [2] inverse_1 [THEN subst])
 apply (rule_tac [2] LIM_inverse)
 apply (simp_all add: divide_inverse [symmetric])