changeset 36498 | c36bbcb00689 |
parent 36407 | d733c1a624f4 |
child 36561 | f91c71982811 |
--- a/src/HOL/Metis_Examples/BigO.thy Wed Apr 28 16:15:45 2010 +0200 +++ b/src/HOL/Metis_Examples/BigO.thy Wed Apr 28 16:47:56 2010 +0200 @@ -206,8 +206,6 @@ qed -sledgehammer_params [sorts] - lemma bigo_alt_def: "O(f) = {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}" by (auto simp add: bigo_def bigo_pos_const)