fixed document;
authorwenzelm
Fri Apr 06 12:45:56 2012 +0200 (2012-04-06)
changeset 473825b902eeb2a29
parent 47381 376b91cdfea8
child 47383 003189cebf12
fixed document;
src/HOL/Library/Polynomial.thy
     1.1 --- a/src/HOL/Library/Polynomial.thy	Fri Apr 06 12:10:50 2012 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Apr 06 12:45:56 2012 +0200
     1.3 @@ -492,7 +492,7 @@
     1.4  
     1.5  subsection {* Multiplication of polynomials *}
     1.6  
     1.7 -text {* TODO: move to Set_Interval.thy *}
     1.8 +(* 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))"