src/HOL/Algebra/UnivPoly.thy
changeset 20282 49c312eaaa11
parent 20217 25b068a99d2b
child 20318 0e0ea63fe768
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Aug 02 13:48:21 2006 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Aug 02 16:50:41 2006 +0200
     1.3 @@ -511,7 +511,7 @@
     1.4        have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
     1.5          by (simp cong: R.finsum_cong add: Pi_def)
     1.6        from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
     1.7 -        by (simp cong: R.finsum_cong add: Pi_def) arith
     1.8 +        by (simp cong: R.finsum_cong add: Pi_def)
     1.9        have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
    1.10          by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
    1.11        show ?thesis