# HG changeset patch
# User hoelzl
# Date 1471536705 -7200
# Node ID 3b0500bd22403be9f29d6350b6c4dc7f7244214a
# Parent  91a0494d8a4a0fb9d95df1572e4f1d267548b048
remove spurious find_theorems

diff -r 91a0494d8a4a -r 3b0500bd2240 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu Aug 18 11:00:36 2016 +0200
+++ b/src/HOL/Deriv.thy	Thu Aug 18 18:11:45 2016 +0200
@@ -2042,7 +2042,7 @@
     by (rule filterlim_inverse_at_top)
   thus ?thesis by simp
 qed
-find_theorems at_top at_bot uminus
+
 lemma lhopital_right_at_top_at_bot:
   fixes f g :: "real \<Rightarrow> real"
   assumes f_0: "LIM x at_right a. f x :> at_top"