only use exhaustive testing in this quickcheck example
authorbulwahn
Wed, 20 Jul 2011 08:16:32 +0200
changeset 43909 7feb72f7bc3e
parent 43908 e18c57d6225d
child 43910 575bf39e078b
only use exhaustive testing in this quickcheck example
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