src/HOL/Library/Polynomial.thy
changeset 47382 5b902eeb2a29
parent 47317 432b29a96f61
child 49834 b27bbb021df1
--- 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))"