--- 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"