src/HOL/Library/Dlist.thy

--- a/src/HOL/Library/Dlist.thy	Tue Dec 20 17:40:15 2011 +0100
+++ b/src/HOL/Library/Dlist.thy	Tue Dec 20 17:40:17 2011 +0100
@@ -180,6 +180,9 @@
 enriched_type map: map
   by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
 
+subsection {* Quickcheck generators *}
+
+quickcheck_generator dlist constructors: empty, insert
 
 hide_const (open) member fold foldr empty insert remove map filter null member length fold