# HG changeset patch # User haftmann # Date 1387827933 -3600 # Node ID d700d054d02215d4c3aded010a334852032e856b # Parent 3324a007863693dae5e879f314170f27068d8f1f convenient printing of polynomial values diff -r 3324a0078636 -r d700d054d022 src/HOL/Library/Polynomial.thy --- 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 \ '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"