src/HOL/Library/BigO.thy
changeset 41865 4e8483cc2cc5
parent 41528 276078f01ada
child 42285 8d91a85b6d91
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Feb 25 12:16:18 2011 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Mon Feb 28 15:06:36 2011 +0000
     1.3 @@ -92,10 +92,7 @@
     1.4    done
     1.5  
     1.6  lemma bigo_zero2: "O(%x.0) = {%x.0}"
     1.7 -  apply (auto simp add: bigo_def) 
     1.8 -  apply (rule ext)
     1.9 -  apply auto
    1.10 -  done
    1.11 +  by (auto simp add: bigo_def) 
    1.12  
    1.13  lemma bigo_plus_self_subset [intro]: 
    1.14    "O(f) \<oplus> O(f) <= O(f)"