# HG changeset patch
# User blanchet
# Date 1272466076 -7200
# Node ID c36bbcb006893c401896ff09e459242cda795445
# Parent  d2e8e5561c35016249d08d0dc7223573cfe183cd
remove removed option

diff -r d2e8e5561c35 -r c36bbcb00689 src/HOL/Metis_Examples/BigO.thy
--- 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)