# HG changeset patch
# User bulwahn
# Date 1324399218 -3600
# Node ID 8748456601197a4c3ad463395646a4d9ec765300
# Parent  e0305e4f02c9c4fb7a8cec0def7e205944f07cc2
adding quickcheck generators in some HOL-Library theories

diff -r e0305e4f02c9 -r 874845660119 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Dec 20 17:40:17 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy	Tue Dec 20 17:40:18 2011 +0100
@@ -1503,6 +1503,8 @@
 
 code_datatype "0::'a::zero poly" pCons
 
+quickcheck_generator poly constructors: "0::'a::zero poly", pCons
+
 declare pCons_0_0 [code_post]
 
 instantiation poly :: ("{zero, equal}") equal
diff -r e0305e4f02c9 -r 874845660119 src/HOL/Library/RBT.thy
--- 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