# HG changeset patch
# User wenzelm
# Date 1243946627 -7200
# Node ID 8991eb94fb0b054a70f221a348d5d8b4ab816327
# Parent  380188f5e75e1f0b91607a7521b56057adbc8af7# Parent  7f65653e3d48da6c1a9bff8018ff66b3b15de6c0
merged

diff -r 7f65653e3d48 -r 8991eb94fb0b src/HOL/Integration.thy
--- a/src/HOL/Integration.thy	Tue Jun 02 14:38:10 2009 +0200
+++ b/src/HOL/Integration.thy	Tue Jun 02 14:43:47 2009 +0200
@@ -432,7 +432,7 @@
     have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
       using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
     also have "\<dots> = rsum D1 f + rsum D2 f"
-      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append ring_simps)
+      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
     finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
       using add_strict_mono[OF rsum1 rsum2] by simp
   }