1.1 --- a/src/HOL/Library/RBT.thy	Tue Dec 20 17:40:17 2011 +0100
     1.2 +++ b/src/HOL/Library/RBT.thy	Tue Dec 20 17:40:18 2011 +0100
     1.3 @@ -169,5 +169,8 @@
     1.4    "distinct (keys t)"
     1.5    by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
     1.6  
     1.7 +subsection {* Quickcheck generators *}
     1.8 +
     1.9 +quickcheck_generator rbt constructors: empty, insert
    1.10  
    1.11  end