diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:51 2014 +0200
@@ -5915,29 +5915,10 @@
   proof -
     fix y
     assume as: "y\<in>cbox (x - ?d) (x + ?d)"
-    {
-      fix i :: 'a
-      assume i: "i \<in> Basis"
-      have "x \<bullet> i \<le> d + y \<bullet> i" "y \<bullet> i \<le> d + x \<bullet> i"
-        using as[unfolded mem_box, THEN bspec[where x=i]] i
-        by (auto simp: inner_simps)
-      then have "1 \<ge> inverse d * (x \<bullet> i - y \<bullet> i)" "1 \<ge> inverse d * (y \<bullet> i - x \<bullet> i)"
-        apply (rule_tac[!] mult_left_le_imp_le[OF _ assms])
-        unfolding mult.assoc[symmetric]
-        using assms
-        by (auto simp add: field_simps)
-      then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
-        "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
-        using `0<d` by (auto simp add: field_simps) }
     then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
-      unfolding mem_box using assms
-      by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
-    then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
-      apply -
-      apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
-      using assms
-      apply auto
-      done
+      using assms by (simp add: mem_box field_simps inner_simps)
+    with `0 < d` show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
+      by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
   next
     fix y z
     assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
@@ -6076,7 +6057,7 @@
           using `0 < t` `2 < t` and `y \<in> s` `w \<in> s`
           by (auto simp add:field_simps)
         also have "\<dots> = (f w + t * f y) / (1 + t)"
-          using `t > 0` unfolding divide_inverse by (auto simp add: field_simps)
+          using `t > 0` by (auto simp add: divide_simps)
         also have "\<dots> < e + f y"
           using `t > 0` * `e > 0` by (auto simp add: field_simps)
         finally have "f x - f y < e" by auto