src/HOL/SetInterval.thy
changeset 23431 25ca91279a9b
parent 23413 5caa2710dd5b
child 23477 f4b83f03cac9
     1.1 --- a/src/HOL/SetInterval.thy	Wed Jun 20 05:06:56 2007 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Jun 20 05:18:39 2007 +0200
     1.3 @@ -756,7 +756,7 @@
     1.4    show ?case by simp
     1.5  next
     1.6    case (Suc n)
     1.7 -  then show ?case by (simp add: right_distrib add_assoc mult_ac)
     1.8 +  then show ?case by (simp add: ring_eq_simps)
     1.9  qed
    1.10  
    1.11  theorem arith_series_general:
    1.12 @@ -779,7 +779,7 @@
    1.13    also from ngt1 
    1.14    have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
    1.15      by (simp only: mult_ac gauss_sum [of "n - 1"])
    1.16 -       (simp add:  mult_ac of_nat_Suc [symmetric])
    1.17 +       (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
    1.18    finally show ?thesis by (simp add: mult_ac add_ac right_distrib)
    1.19  next
    1.20    assume "\<not>(n > 1)"