--- 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
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Thu Nov 10 17:26:15 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Thu Nov 10 17:26:17 2011 +0100
@@ -66,6 +66,11 @@
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
oops
+lemma "a # xs = ys @ [a] ==> EX zs. xs = zs @ [a] & ys = a#zs"
+quickcheck[narrowing, expect = counterexample]
+quickcheck[exhaustive, random, expect = no_counterexample]
+oops
+
subsection {* Simple list examples *}
lemma "rev xs = xs"