diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -3299,7 +3299,7 @@
   then have "ball (x - e *\<^sub>R (x - c)) (e*d) \<inter> affine hull S \<subseteq> S"
     by auto
   moreover have "e * d > 0"
-    using `e > 0` `d > 0` by (rule mult_pos_pos)
+    using `e > 0` `d > 0` by simp
   moreover have c: "c \<in> S"
     using assms rel_interior_subset by auto
   moreover from c have "x - e *\<^sub>R (x - c) \<in> S"
@@ -3453,7 +3453,7 @@
     case True
     then show ?thesis using `e > 0` `d > 0`
       apply (rule_tac bexI[where x=x])
-      apply (auto intro!: mult_pos_pos)
+      apply (auto)
       done
   next
     case False
@@ -3473,8 +3473,7 @@
     next
       case False
       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
-        using `e \<le> 1` `e > 0` `d > 0`
-        by (auto intro!:mult_pos_pos divide_pos_pos)
+        using `e \<le> 1` `e > 0` `d > 0` by (auto)
       then obtain y where "y \<in> S" "y \<noteq> x" "dist y x < e * d / (1 - e)"
         using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
       then show ?thesis
@@ -3602,7 +3601,7 @@
     then have e1: "e1 > 0" "\<And>x. e1 * norm (f x) \<le> norm x"
       using K pos_le_divide_eq[of e1] by auto
     def e \<equiv> "e1 * e2"
-    then have "e > 0" using e1 e2 mult_pos_pos by auto
+    then have "e > 0" using e1 e2 by auto
     {
       fix y
       assume y: "y \<in> cball x e \<inter> affine hull S"
@@ -3645,8 +3644,7 @@
         subspace_span[of S] closed_subspace[of "span S"]
       by auto
     def e \<equiv> "e1 * e2"
-    then have "e > 0"
-      using e1 e2 mult_pos_pos by auto
+    hence "e > 0" using e1 e2 by auto
     {
       fix y
       assume y: "y \<in> cball (f x) e \<inter> affine hull (f ` S)"
@@ -6091,7 +6089,7 @@
       }
       ultimately show ?thesis by auto
     qed (insert `0<e`, auto)
-  qed (insert `0<e` `0<k` `0<B`, auto simp add:field_simps intro!:mult_pos_pos)
+  qed (insert `0<e` `0<k` `0<B`, auto simp: field_simps)
 qed
 
 
@@ -6513,7 +6511,7 @@
       using assms(3-5)
       apply auto
       done
-  qed (rule mult_pos_pos, insert `e>0` `d>0`, auto)
+  qed (insert `e>0` `d>0`, auto)
 qed
 
 lemma mem_interior_closure_convex_shrink:
@@ -6533,7 +6531,7 @@
     then show ?thesis
       using `e > 0` `d > 0`
       apply (rule_tac bexI[where x=x])
-      apply (auto intro!: mult_pos_pos)
+      apply (auto)
       done
   next
     case False
@@ -6553,8 +6551,7 @@
     next
       case False
       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
-        using `e \<le> 1` `e > 0` `d > 0`
-        by (auto intro!:mult_pos_pos divide_pos_pos)
+        using `e \<le> 1` `e > 0` `d > 0` by auto
       then obtain y where "y \<in> s" "y \<noteq> x" "dist y x < e * d / (1 - e)"
         using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
       then show ?thesis