Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove spurious find_theorems
authorhoelzl
Thu, 18 Aug 2016 18:11:45 +0200
changeset 63717 3b0500bd2240
parent 63716 91a0494d8a4a
child 63718 600cf5c8f2ba
remove spurious find_theorems
src/HOL/Deriv.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle