removed junk;

--- a/src/HOL/Library/Landau_Symbols.thy	Fri Jul 27 22:23:37 2018 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy	Fri Jul 27 23:04:27 2018 +0200
@@ -630,8 +630,6 @@
   {
     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
     show "L F (f) = L F (g)" unfolding L_def
-      
-      thm eventually_subst A
       by (subst eventually_subst'[OF A]) (rule refl)
   }
   {