--- a/src/HOL/Algebra/UnivPoly.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Aug 30 03:19:08 2006 +0200
@@ -513,7 +513,7 @@
have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
by (simp cong: R.finsum_cong add: Pi_def)
from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
- by (simp cong: R.finsum_cong add: Pi_def)
+ by (simp cong: R.finsum_cong add: Pi_def) arith
have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
show ?thesis