src/HOL/Smallcheck.thy
changeset 40915 a4c956d1f91f
parent 40914 0c071c5202b5
child 41085 a549ff1d4070
--- 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