Removed usage of normalizating locales.

--- a/src/HOL/Metis_Examples/BT.thy	Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Metis_Examples/BT.thy	Tue May 11 19:21:05 2010 +0200
@@ -88,7 +88,7 @@
   case Lf thus ?case by (metis reflect.simps(1))
 next
   case (Br a t1 t2) thus ?case
-    by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+    by (metis add_commute n_nodes.simps(2) reflect.simps(2))
 qed
 
 declare [[ atp_problem_prefix = "BT__depth_reflect" ]]

--- a/src/HOL/Metis_Examples/BigO.thy	Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy	Tue May 11 19:21:05 2010 +0200
@@ -41,7 +41,7 @@
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
   have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
-  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
   have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
   have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
     by (metis abs_mult)
@@ -66,11 +66,11 @@
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto);
+  apply (rule_tac x = "abs c" in exI, auto)
 proof -
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
   have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
     by (metis abs_mult)
   have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
@@ -92,7 +92,7 @@
 proof -
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
   have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
   hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
   hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
@@ -111,7 +111,7 @@
 proof -
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
   hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
     by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
   hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
@@ -131,26 +131,26 @@
   apply (rule conjI)
   apply (rule mult_pos_pos)
   apply (assumption)+ 
-(*sledgehammer*);
+(*sledgehammer*)
   apply (rule allI)
   apply (drule_tac x = "xa" in spec)+
-  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))");
+  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
   apply (erule order_trans)
   apply (simp add: mult_ac)
   apply (rule mult_left_mono, assumption)
-  apply (rule order_less_imp_le, assumption);
+  apply (rule order_less_imp_le, assumption)
 done
 
 
 declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
 lemma bigo_refl [intro]: "f : O(f)"
 apply (auto simp add: bigo_def)
-by (metis normalizing.mul_1 order_refl)
+by (metis mult_1 order_refl)
 
 declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
 lemma bigo_zero: "0 : O(g)"
 apply (auto simp add: bigo_def func_zero)
-by (metis normalizing.mul_0 order_refl)
+by (metis mult_zero_left order_refl)
 
 lemma bigo_zero2: "O(%x.0) = {%x.0}"
   apply (auto simp add: bigo_def) 
@@ -237,7 +237,7 @@
   apply (rule bigo_plus_subset)
   apply (simp add: bigo_alt_def set_plus_def func_plus)
   apply clarify 
-(*sledgehammer*); 
+(*sledgehammer*) 
   apply (rule_tac x = "max c ca" in exI)
   apply (rule conjI)
    apply (metis Orderings.less_max_iff_disj)
@@ -307,7 +307,7 @@
  apply (auto simp add: diff_minus fun_Compl_def func_plus)
  prefer 2
  apply (drule_tac x = x in spec)+
- apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
+ apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans)
 proof -
   fix x :: 'a
   assume "\<forall>x. lb x \<le> f x"
@@ -318,13 +318,13 @@
 lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
 apply (unfold bigo_def)
 apply auto
-by (metis normalizing.mul_1 order_refl)
+by (metis mult_1 order_refl)
 
 declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
 lemma bigo_abs2: "f =o O(%x. abs(f x))"
 apply (unfold bigo_def)
 apply auto
-by (metis normalizing.mul_1 order_refl)
+by (metis mult_1 order_refl)
  
 lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
 proof -

--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 11 19:21:05 2010 +0200
@@ -1877,7 +1877,7 @@
       using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
       unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
       apply (rule mult_left_le_imp_le[of "1 - u"])
-      unfolding normalizing.mul_a using `u<1` by auto
+      unfolding mult_assoc[symmetric] using `u<1` by auto
     thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
       using as unfolding scaleR_scaleR by auto qed auto
   thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 11 19:21:05 2010 +0200
@@ -698,7 +698,8 @@
     unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto
   then guess x .. note x=this
   show ?thesis proof(cases "f a = f b")
-    case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:normalizing.semiring_rules)
+    case False
+    have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add: power2_eq_square)
     also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
     also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
     also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue May 11 19:21:05 2010 +0200
@@ -2533,7 +2533,7 @@
           show "content x \<ge> 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le)
         qed have **:"norm (1::real) \<le> 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit]
         note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]]
-        note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
+        note this[unfolded real_scaleR_def real_norm_def mult_1_right mult_1, of k c d] note le_less_trans[OF this d(2)]
         from this[unfolded abs_of_nonneg[OF *]] show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x $ k - c\<bar> \<le> d})) < e"
           apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym])
           apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p'']
@@ -4723,7 +4723,7 @@
   have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
     \<longrightarrow> norm(ig) < dia + e" 
   proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
-      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a
+      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding add_assoc[symmetric]
       apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
       apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
   qed note norm=this[rule_format]

--- a/src/HOL/Probability/Lebesgue.thy	Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy	Tue May 11 19:21:05 2010 +0200
@@ -939,17 +939,17 @@
   proof safe
     fix t assume t: "t \<in> space M"
     { fix m n :: nat assume "m \<le> n"
-      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto
+      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding power_add[symmetric] by auto
       have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
         apply (subst *)
-        apply (subst normalizing.mul_a)
+        apply (subst mult_assoc[symmetric])
         apply (subst real_of_nat_le_iff)
         apply (rule le_mult_natfloor)
         using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
       hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
         apply (subst *)
-        apply (subst (3) normalizing.mul_c)
-        apply (subst normalizing.mul_a)
+        apply (subst (3) mult_commute)
+        apply (subst mult_assoc[symmetric])
         by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
     thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
       by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)