src/HOL/Library/Dlist.thy
changeset 45927 e0305e4f02c9
parent 45694 4a8743618257
child 45990 b7b905b23b2a
     1.1 --- a/src/HOL/Library/Dlist.thy	Tue Dec 20 17:40:15 2011 +0100
     1.2 +++ b/src/HOL/Library/Dlist.thy	Tue Dec 20 17:40:17 2011 +0100
     1.3 @@ -180,6 +180,9 @@
     1.4  enriched_type map: map
     1.5    by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
     1.6  
     1.7 +subsection {* Quickcheck generators *}
     1.8 +
     1.9 +quickcheck_generator dlist constructors: empty, insert
    1.10  
    1.11  hide_const (open) member fold foldr empty insert remove map filter null member length fold
    1.12