# HG changeset patch
# User haftmann
# Date 1325152076 -3600
# Node ID ac6bae9fdc2f0a2c11b03ed576284b773f08305a
# Parent  51b2f3412a03123fd826d053e3aa5d2448041393
tuned declaration

diff -r 51b2f3412a03 -r ac6bae9fdc2f src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Dec 29 10:47:56 2011 +0100
@@ -147,7 +147,7 @@
 apply (rule le_degree, simp)
 done
 
-lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
+lemma pCons_0_0 [simp, code_post]: "pCons 0 0 = 0"
 by (rule poly_ext, simp add: coeff_pCons split: nat.split)
 
 lemma pCons_eq_iff [simp]:
@@ -1505,8 +1505,6 @@
 
 quickcheck_generator poly constructors: "0::'a::zero poly", pCons
 
-declare pCons_0_0 [code_post]
-
 instantiation poly :: ("{zero, equal}") equal
 begin