# HG changeset patch
# User hoelzl
# Date 1243946225 -7200
# Node ID 380188f5e75e1f0b91607a7521b56057adbc8af7
# Parent  46da733309136e238c0167848c0fefa802de00c4
use algebra_simps instead of ring_simps

diff -r 46da73330913 -r 380188f5e75e src/HOL/Integration.thy
--- a/src/HOL/Integration.thy	Tue Jun 02 14:00:24 2009 +0200
+++ b/src/HOL/Integration.thy	Tue Jun 02 14:37:05 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
   }