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)