src/HOL/Library/Polynomial.thy
changeset 46031 ac6bae9fdc2f
parent 45928 874845660119
child 47002 9435d419109a
     1.1 --- a/src/HOL/Library/Polynomial.thy	Thu Dec 29 10:47:55 2011 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Dec 29 10:47:56 2011 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4  apply (rule le_degree, simp)
     1.5  done
     1.6  
     1.7 -lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
     1.8 +lemma pCons_0_0 [simp, code_post]: "pCons 0 0 = 0"
     1.9  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
    1.10  
    1.11  lemma pCons_eq_iff [simp]:
    1.12 @@ -1505,8 +1505,6 @@
    1.13  
    1.14  quickcheck_generator poly constructors: "0::'a::zero poly", pCons
    1.15  
    1.16 -declare pCons_0_0 [code_post]
    1.17 -
    1.18  instantiation poly :: ("{zero, equal}") equal
    1.19  begin
    1.20