Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Ln.thy
changeset 31338 d41a8ba25b67
parent 30273 ecd6f0ca62ea
child 31883 9e5bdbae677d 
--- a/src/HOL/Ln.thy	Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/Ln.thy	Fri May 29 09:22:56 2009 -0700
@@ -343,7 +343,7 @@
 done
 
 lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
-  apply (unfold deriv_def, unfold LIM_def, clarsimp)
+  apply (unfold deriv_def, unfold LIM_eq, clarsimp)
   apply (rule exI)
   apply (rule conjI)
   prefer 2
isabelle