| changeset 54855 | d700d054d022 |
| parent 54489 | 03ff4d1e6784 |
| child 54856 | 356b4c0a2061 |
--- a/src/HOL/Library/Polynomial.thy Mon Dec 23 18:37:51 2013 +0100 +++ b/src/HOL/Library/Polynomial.thy Mon Dec 23 20:45:33 2013 +0100 @@ -367,8 +367,8 @@ primrec Poly :: "'a::zero list \<Rightarrow> 'a poly" where - "Poly [] = 0" -| "Poly (a # as) = pCons a (Poly as)" + [code_post]: "Poly [] = 0" +| [code_post]: "Poly (a # as) = pCons a (Poly as)" lemma Poly_replicate_0 [simp]: "Poly (replicate n 0) = 0"