declare tester in this quickcheck example
authorbulwahn
Mon, 18 Jul 2011 11:38:14 +0200
changeset 43890 eba9c3b1f84a
parent 43889 90d24cafb05d
child 43891 4690f76f327a
declare tester in this quickcheck example
src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Jul 18 11:38:14 2011 +0200
@@ -361,7 +361,7 @@
 begin
 
 lemma "False"
-quickcheck[expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 end