diff -r c3b6e69da386 -r e5104b436ea1 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Feb 28 22:10:57 2011 +0100
@@ -6,7 +6,6 @@
 theory Integration
 imports
   Derivative
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
@@ -14,8 +13,6 @@
 declare [[smt_fixed=true]]
 declare [[smt_oracle=false]]
 
-setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
-
 (*declare not_less[simp] not_le[simp]*)
 
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -2879,7 +2876,7 @@
 lemma operative_1_lt: assumes "monoidal opp"
   shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and>
                 (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f{a..c})(f{c..b}) = f {a..b}))"
-  unfolding operative_def content_eq_0 DIM_real less_one dnf_simps(39,41) Eucl_real_simps
+  unfolding operative_def content_eq_0 DIM_real less_one simp_thms(39,41) Eucl_real_simps
     (* The dnf_simps simplify "\<exists> x. x= _ \<and> _" and "\<forall>k. k = _ \<longrightarrow> _" *)
 proof safe fix a b c::"real" assume as:"\<forall>a b c. f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c}))
     (f ({a..b} \<inter> {x. c \<le> x}))" "a < c" "c < b"
@@ -4354,7 +4351,7 @@
   "(\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)"
   and p:"p tagged_partial_division_of {a..b}" "d fine p"
   shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
-proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by arith }
+proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) }
   fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
   have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastsimp
   note partial_division_of_tagged_division[OF p(1)] this