--- a/src/HOL/ex/Quickcheck_Examples.thy Thu Nov 10 17:26:15 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Thu Nov 10 17:26:17 2011 +0100
@@ -380,4 +380,22 @@
end
+subsection {* Examples with HOL quantifiers *}
+
+lemma
+ "\<forall> xs ys. xs = [] --> xs = ys"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+
end