src/HOL/Quickcheck_Exhaustive.thy
changeset 43882 05d5696f177f
parent 42310 c664cc5cc5e9
child 45450 dc2236b19a3d
--- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -452,7 +452,7 @@
 
 setup {* Exhaustive_Generators.setup *}
 
-declare [[quickcheck_tester = exhaustive]]
+declare [[quickcheck_batch_tester = exhaustive]]
 
 hide_fact orelse_def catch_match_def
 no_notation orelse (infixr "orelse" 55)