1.1 --- a/src/HOL/Library/Polynomial.thy	Fri Feb 27 16:05:40 2009 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Feb 27 15:37:56 2009 -0800
     1.3 @@ -106,6 +106,7 @@
     1.4  translations
     1.5    "[:x, xs:]" == "CONST pCons x [:xs:]"
     1.6    "[:x:]" == "CONST pCons x 0"
     1.7 +  "[:x:]" <= "CONST pCons x (_constrain 0 t)"
     1.8  
     1.9  lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
    1.10    unfolding Poly_def by (auto split: nat.split)