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"