diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Wed Feb 18 22:46:47 2015 +0100
@@ -23,8 +23,8 @@
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
     \<forall>x. abs (h x) \<le> c * abs (f x))
     \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
-by (metis (no_types) abs_ge_zero
-      comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral
+  by (metis (no_types) abs_ge_zero
+      algebra_simps mult.comm_neutral
       mult_nonpos_nonneg not_leE order_trans zero_less_one)
 
 (*** Now various verions with an increasing shrink factor ***)
@@ -131,8 +131,8 @@
 lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
 apply (auto simp add: bigo_alt_def)
 apply (rule_tac x = "ca * c" in exI)
-by (metis comm_semiring_1_class.normalizing_semiring_rules(7,19)
-          mult_le_cancel_left_pos order_trans mult_pos_pos)
+apply (metis algebra_simps mult_le_cancel_left_pos order_trans mult_pos_pos)
+done
 
 lemma bigo_refl [intro]: "f : O(f)"
 unfolding bigo_def mem_Collect_eq
@@ -232,9 +232,9 @@
 apply (rule set_minus_imp_plus)
 apply (rule bigo_bounded)
  apply (metis add_le_cancel_left diff_add_cancel diff_self minus_apply
-              comm_semiring_1_class.normalizing_semiring_rules(24))
+              algebra_simps)
 by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
-          comm_semiring_1_class.normalizing_semiring_rules(24))
+          algebra_simps)
 
 lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
 apply (unfold bigo_def)
@@ -339,9 +339,7 @@
     then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
       by auto
     also have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) = h"
-      apply (simp add: func_times)
-      by (metis (lifting, no_types) a eq_divide_imp ext
-                comm_semiring_1_class.normalizing_semiring_rules(7))
+      by (simp add: func_times fun_eq_iff a)
     finally show "h : f *o O(g)".
   qed
 qed
@@ -368,9 +366,8 @@
 by (auto simp add: bigo_def fun_Compl_def)
 
 lemma bigo_minus2: "f : g +o O(h) \<Longrightarrow> -f : -g +o O(h)"
-by (metis (no_types) bigo_elt_subset bigo_minus bigo_mult4 bigo_refl
-          comm_semiring_1_class.normalizing_semiring_rules(11) minus_mult_left
-          set_plus_mono_b)
+by (metis (no_types, lifting) bigo_minus diff_minus_eq_add minus_add_distrib
+    minus_minus set_minus_imp_plus set_plus_imp_minus)
 
 lemma bigo_minus3: "O(-f) = O(f)"
 by (metis bigo_elt_subset bigo_minus bigo_refl equalityI minus_minus)