preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)
authorbulwahn
Wed, 22 Feb 2012 09:35:01 +0100
changeset 46587 d3bcc356cc60
parent 46586 abbec6fa25c8
child 46588 4895d7f1be42
preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)
src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Feb 22 08:05:28 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Feb 22 09:35:01 2012 +0100
@@ -512,7 +512,7 @@
 
 (* setup *)
 
-val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
+val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
 
 val setup =
   Code.datatype_interpretation ensure_partial_term_of