author | huffman |
Fri, 27 Feb 2009 15:39:35 -0800 | |
changeset 30156 | c621f8b6f4e6 |
parent 30155 | f65dc19cd5f0 (diff) |
parent 30154 | 9193a48d3f95 (current diff) |
child 30157 | 40919ebde2c9 |
--- a/src/HOL/Library/Polynomial.thy Fri Feb 27 20:00:54 2009 +0100 +++ b/src/HOL/Library/Polynomial.thy Fri Feb 27 15:39:35 2009 -0800 @@ -106,6 +106,7 @@ translations "[:x, xs:]" == "CONST pCons x [:xs:]" "[:x:]" == "CONST pCons x 0" + "[:x:]" <= "CONST pCons x (_constrain 0 t)" lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly" unfolding Poly_def by (auto split: nat.split)