| changeset 45928 | 874845660119 |
| parent 45694 | 4a8743618257 |
| child 46031 | ac6bae9fdc2f |
--- a/src/HOL/Library/Polynomial.thy Tue Dec 20 17:40:17 2011 +0100 +++ b/src/HOL/Library/Polynomial.thy Tue Dec 20 17:40:18 2011 +0100 @@ -1503,6 +1503,8 @@ 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