# HG changeset patch
# User bulwahn
# Date 1310981894 -7200
# Node ID eba9c3b1f84a76050f8e7c3fd49bbdbc9544ad20
# Parent  90d24cafb05d84ed0e621865a8bf9c918ee8758e
declare tester in this quickcheck example

diff -r 90d24cafb05d -r eba9c3b1f84a 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