src/HOL/Library/BigO.thy
changeset 56796 9f84219715a7
parent 56544 b60d5d119489
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Library/BigO.thy	Tue Apr 29 21:54:26 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Tue Apr 29 22:50:55 2014 +0200
     1.3 @@ -390,7 +390,7 @@
     1.4      also have "\<dots> \<subseteq> O(g) + O(g)"
     1.5      proof -
     1.6        from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
     1.7 -      thus ?thesis by (auto del: subsetI)
     1.8 +      then show ?thesis by (auto del: subsetI)
     1.9      qed
    1.10      also have "\<dots> \<subseteq> O(g)" by simp
    1.11      finally show ?thesis .