--- a/src/HOL/Quickcheck.thy Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Quickcheck.thy Fri Dec 03 08:40:47 2010 +0100
@@ -129,6 +129,7 @@
use "Tools/quickcheck_generators.ML"
setup Quickcheck_Generators.setup
+declare [[quickcheck_tester = random]]
subsection {* Code setup *}
--- a/src/HOL/Smallcheck.thy Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Smallcheck.thy Fri Dec 03 08:40:47 2010 +0100
@@ -135,6 +135,8 @@
setup {* Smallvalue_Generators.setup *}
+declare [[quickcheck_tester = exhaustive]]
+
hide_fact orelse_def catch_match_def
hide_const (open) orelse catch_match