src/HOL/Library/Polynomial.thy
changeset 47317 432b29a96f61
parent 47108 2a1953f0d20d
child 47382 5b902eeb2a29
     1.1 --- a/src/HOL/Library/Polynomial.thy	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Apr 03 15:15:00 2012 +0200
     1.3 @@ -492,7 +492,7 @@
     1.4  
     1.5  subsection {* Multiplication of polynomials *}
     1.6  
     1.7 -text {* TODO: move to SetInterval.thy *}
     1.8 +text {* TODO: move to Set_Interval.thy *}
     1.9  lemma setsum_atMost_Suc_shift:
    1.10    fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
    1.11    shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"