diff -r c27b0b37041a -r 4e8483cc2cc5 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Library/BigO.thy	Mon Feb 28 15:06:36 2011 +0000
@@ -92,10 +92,7 @@
   done
 
 lemma bigo_zero2: "O(%x.0) = {%x.0}"
-  apply (auto simp add: bigo_def) 
-  apply (rule ext)
-  apply auto
-  done
+  by (auto simp add: bigo_def) 
 
 lemma bigo_plus_self_subset [intro]: 
   "O(f) \<oplus> O(f) <= O(f)"