# HG changeset patch
# User huffman
# Date 1179647456 -7200
# Node ID 5e40f1e9958a4c1219a5cb15b57f00b9cf9506e9
# Parent  17f7d831efe2204ddfc1828623de658eb8e3458c
remove obsolete DERIV_ln lemmas

diff -r 17f7d831efe2 -r 5e40f1e9958a src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 09:21:04 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 09:50:56 2007 +0200
@@ -2115,36 +2115,6 @@
 declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
 
 
-subsection{*A Few Theorems Involving Ln, Derivatives, etc.*}
-
-lemma lemma_DERIV_ln:
-     "DERIV ln z :> l ==> DERIV (%x. exp (ln x)) z :> exp (ln z) * l"
-by (erule DERIV_fun_exp)
-
-lemma DERIV_exp_ln_one: "0 < z ==> DERIV (%x. exp (ln x)) z :> 1"
-apply (simp add: deriv_def)
-apply (rule LIM_equal2 [OF _ _ LIM_const], assumption)
-apply simp
-done
-
-lemma lemma_DERIV_ln2:
-     "[| 0 < z; DERIV ln z :> l |] ==>  exp (ln z) * l = 1"
-apply (rule DERIV_unique)
-apply (rule lemma_DERIV_ln)
-apply (rule_tac [2] DERIV_exp_ln_one, auto)
-done
-
-lemma lemma_DERIV_ln3:
-     "[| 0 < z; DERIV ln z :> l |] ==>  l = 1/(exp (ln z))"
-apply (rule_tac c1 = "exp (ln z)" in real_mult_left_cancel [THEN iffD1])
-apply (auto intro: lemma_DERIV_ln2 simp del: exp_ln)
-done
-
-lemma lemma_DERIV_ln4: "[| 0 < z; DERIV ln z :> l |] ==>  l = 1/z"
-apply (rule_tac t = z in exp_ln_iff [THEN iffD2, THEN subst])
-apply (auto intro: lemma_DERIV_ln3 simp del: exp_ln)
-done
-
 subsection {* Theorems about Limits *}
 
 (* need to rename second isCont_inverse *)