src/HOL/Library/Polynomial.thy

 apply (rule degree_le, simp add: coeff_pCons split: nat.split)
 apply (rule order_antisym [OF degree_pCons_le])
 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]:
   "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
 proof (safe)

 
 code_datatype "0::'a::zero poly" pCons
 
 quickcheck_generator poly constructors: "0::'a::zero poly", pCons
 
-declare pCons_0_0 [code_post]
-
 instantiation poly :: ("{zero, equal}") equal
 begin
 
 definition
   "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"