src/HOL/Library/Polynomial.thy
changeset 63145 703edebd1d92
parent 63060 293ede07b775
child 63317 ca187a9f66da
--- 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