src/HOL/SetInterval.thy
changeset 23477 f4b83f03cac9
parent 23431 25ca91279a9b
child 23496 84e9216a6d0e
     1.1 --- a/src/HOL/SetInterval.thy	Fri Jun 22 22:41:17 2007 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Sat Jun 23 19:33:22 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: ring_eq_simps)
     1.8 +  then show ?case by (simp add: ring_simps)
     1.9  qed
    1.10  
    1.11  theorem arith_series_general: