diff -r c3b6e69da386 -r e5104b436ea1 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Feb 28 22:10:57 2011 +0100
@@ -7,7 +7,6 @@
 theory Euclidean_Space
 imports
   Complex_Main
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   "~~/src/HOL/Library/Infinite_Set"
   "~~/src/HOL/Library/Inner_Product"
   L2_Norm
@@ -48,7 +47,8 @@
     by (metis linorder_linear not_le)
     have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
     have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
-    have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo
+    have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
+    then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
     {assume le2: "f l \<in> e2"
       from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
       hence lap: "l - a > 0" using alb by arith
@@ -56,8 +56,10 @@
         e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
       from dst[OF alb e(1)] obtain d where
         d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" using lap d(1)
-        apply ferrack by arith
+      let ?d' = "min (d/2) ((l - a)/2)"
+      have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
+        by (simp add: min_max.less_infI2)
+      then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
       then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
       from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
       from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
@@ -72,7 +74,8 @@
         e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
       from dst[OF alb e(1)] obtain d where
         d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo
+      have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
+      then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
       then obtain d' where d': "d' > 0" "d' < d" by metis
       from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
       hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
@@ -1995,7 +1998,7 @@
         by (simp add: mult_less_0_iff)
       with B[rule_format, of "(\<chi>\<chi> i. 1)::'a"] norm_ge_zero[of "f ((\<chi>\<chi> i. 1)::'a)"] have False by simp
     }
-    then have Bp: "B \<ge> 0" by ferrack
+    then have Bp: "B \<ge> 0" by (metis not_leE)
     {fix x::"'a"
       have "norm (f x) \<le> ?K *  norm x"
       using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp