removed junk;
authorwenzelm
Fri Jul 27 23:04:27 2018 +0200 (11 months ago)
changeset 686968a071eeddb2a
parent 68695 9072bfd24d8f
child 68697 d81a5da01796
removed junk;
src/HOL/Library/Landau_Symbols.thy
     1.1 --- a/src/HOL/Library/Landau_Symbols.thy	Fri Jul 27 22:23:37 2018 +0200
     1.2 +++ b/src/HOL/Library/Landau_Symbols.thy	Fri Jul 27 23:04:27 2018 +0200
     1.3 @@ -630,8 +630,6 @@
     1.4    {
     1.5      fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
     1.6      show "L F (f) = L F (g)" unfolding L_def
     1.7 -      
     1.8 -      thm eventually_subst A
     1.9        by (subst eventually_subst'[OF A]) (rule refl)
    1.10    }
    1.11    {