--- a/src/HOL/ex/Quickcheck_Examples.thy Mon Dec 05 12:36:21 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Mon Dec 05 12:36:22 2011 +0100
@@ -413,22 +413,20 @@
"xs = [] ==> hd xs \<noteq> x"
quickcheck[exhaustive, expect = no_counterexample]
quickcheck[random, report = false, expect = no_counterexample]
-quickcheck[random, report = true, expect = counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
oops
lemma
"xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
oops
lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
oops
text {* with the simple testing scheme *}
@@ -438,19 +436,16 @@
lemma
"xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
oops
lemma
"xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
oops
lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
oops
declare [[quickcheck_full_support = true]]