| 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