| changeset 46565 | ad21900e0ee9 |
| parent 46133 | d9fe85d3d2cd |
| child 48282 | 39bfb2844b9e |
--- a/src/HOL/Library/Dlist.thy Tue Feb 21 11:25:48 2012 +0100 +++ b/src/HOL/Library/Dlist.thy Tue Feb 21 12:20:33 2012 +0100 @@ -182,7 +182,7 @@ subsection {* Quickcheck generators *} -quickcheck_generator dlist constructors: empty, insert +quickcheck_generator dlist predicate: distinct constructors: empty, insert hide_const (open) member fold foldr empty insert remove map filter null member length fold