# 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