--- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Nov 03 10:24:06 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Nov 03 10:36:20 2009 +0100
@@ -5,6 +5,31 @@
section {* Sets *}
+lemma "x \<in> {(1::nat)} ==> False"
+quickcheck[generator=predicate_compile]
+oops
+
+lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
+oops
+
+lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
+quickcheck[generator=predicate_compile]
+oops
+
+lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x <= Suc 0"
+quickcheck[generator=predicate_compile]
+oops
+
+section {* Numerals *}
+
+lemma
+ "x \<in> {1, 2, (3::nat)} ==> x < 3"
+(*quickcheck[generator=predicate_compile]*)
+oops
+lemma
+ "x \<in> {1, 2} \<union> {3, 4} ==> x > 4"
+(*quickcheck[generator=predicate_compile]*)
+oops
section {* Context Free Grammar *}