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