# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID a4c956d1f91f28751fed2bce51e98df08b43ae9b
# Parent  0c071c5202b5bb630f878f3f36dd794236bfb6f8
declaring quickcheck testers as default after their setup

diff -r 0c071c5202b5 -r a4c956d1f91f src/HOL/Quickcheck.thy
--- 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 *}
 
diff -r 0c071c5202b5 -r a4c956d1f91f src/HOL/Smallcheck.thy
--- 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