# 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 \<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"