src/HOL/Library/BigO.thy

     then have "f +o O(g) \<subseteq> O(f) + O(g)"
       by (auto del: subsetI)
     also have "\<dots> \<subseteq> O(g) + O(g)"
     proof -
       from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
-      thus ?thesis by (auto del: subsetI)
+      then show ?thesis by (auto del: subsetI)
     qed
     also have "\<dots> \<subseteq> O(g)" by simp
     finally show ?thesis .
   qed
 qed