# HG changeset patch
# User wenzelm
# Date 1333709156 -7200
# Node ID 5b902eeb2a29092bc606f1c9a54d4100c7e445da
# Parent  376b91cdfea85a6640272b5b3817249f5e2e812c
fixed document;

diff -r 376b91cdfea8 -r 5b902eeb2a29 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))"