src/HOL/Library/RBT.thy
changeset 45928 874845660119
parent 45694 4a8743618257
child 46133 d9fe85d3d2cd
--- a/src/HOL/Library/RBT.thy	Tue Dec 20 17:40:17 2011 +0100
+++ b/src/HOL/Library/RBT.thy	Tue Dec 20 17:40:18 2011 +0100
@@ -169,5 +169,8 @@
   "distinct (keys t)"
   by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
 
+subsection {* Quickcheck generators *}
+
+quickcheck_generator rbt constructors: empty, insert
 
 end