fixed document;
authorwenzelm
Fri, 06 Apr 2012 12:45:56 +0200
changeset 47382 5b902eeb2a29
parent 47381 376b91cdfea8
child 47383 003189cebf12
fixed document;
src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Apr 06 12:10:50 2012 +0200
+++ b/src/HOL/Library/Polynomial.thy	Fri Apr 06 12:45:56 2012 +0200
@@ -492,7 +492,7 @@
 
 subsection {* Multiplication of polynomials *}
 
-text {* TODO: move to Set_Interval.thy *}
+(* TODO: move to Set_Interval.thy *)
 lemma setsum_atMost_Suc_shift:
   fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
   shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"