# HG changeset patch
# User bulwahn
# Date 1311142592 -7200
# Node ID 7feb72f7bc3e546422e9859a33e0ba9ee3e25b5d
# Parent  e18c57d6225daeac2166073c5b0630d4c43c3c37
only use exhaustive testing in this quickcheck example

diff -r e18c57d6225d -r 7feb72f7bc3e src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Jul 20 00:37:42 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Jul 20 08:16:32 2011 +0200
@@ -350,7 +350,7 @@
 begin
 
 lemma "False"
-quickcheck[expect = no_counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
 oops
 
 end