# HG changeset patch
# User haftmann
# Date 1265788165 -3600
# Node ID 96a21dd3b34929d706b0dfbb6ad21e0cad6f9c54
# Parent  894e82be8d05ccb8b7390dfa0e967655c1610b7b
rely less on ordered rewriting

diff -r 894e82be8d05 -r 96a21dd3b349 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Feb 10 08:49:25 2010 +0100
@@ -2950,7 +2950,8 @@
                (\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i (real c) * (xs!x - real c)^i) +
                inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - real c)^Suc n" (is "_ = ?T")
         unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
-        by (auto simp add: algebra_simps setsum_right_distrib[symmetric])
+        by (auto simp add: algebra_simps)
+          (simp only: mult_left_commute [of _ "inverse (real k)"] setsum_right_distrib [symmetric])
       finally have "?T \<in> {real l .. real u}" . }
     thus ?thesis using DERIV by blast
   qed