# HG changeset patch
# User wenzelm
# Date 1532725467 -7200
# Node ID 8a071eeddb2a08e7797159baf1b027cfd0cef6d6
# Parent  9072bfd24d8f71c5803481cb5a94c15e6eb8f4ef
removed junk;

diff -r 9072bfd24d8f -r 8a071eeddb2a src/HOL/Library/Landau_Symbols.thy
--- 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)
   }
   {