# HG changeset patch
# User bulwahn
# Date 1291629165 -3600
# Node ID 890fefa597af2bfd9ed90d3e645d91c34b03bf9a
# Parent  ce78ef6a909b3f51d10bf5d07af4d6077fc07d11
removing declaration in quickcheck to really enable exhaustive testing

diff -r ce78ef6a909b -r 890fefa597af src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Mon Dec 06 10:52:44 2010 +0100
+++ b/src/HOL/Quickcheck.thy	Mon Dec 06 10:52:45 2010 +0100
@@ -129,7 +129,6 @@
 use "Tools/quickcheck_generators.ML"
 setup Quickcheck_Generators.setup
 
-declare [[quickcheck_tester = random]]
 
 subsection {* Code setup *}