--- a/src/HOL/Library/Polynomial.thy Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy Wed May 25 11:49:40 2016 +0200
@@ -443,7 +443,7 @@
by (simp add: is_zero_def null_def)
subsubsection \<open>Reconstructing the polynomial from the list\<close>
- -- \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
+ \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
where