activating narrowing-based quickcheck by default
authorbulwahn
Thu, 18 Aug 2011 12:06:17 +0200
changeset 45135360fcbb1aa01
parent 45134 971d1be5d5ce
child 45136 336752fb25df
child 45143 4846f3f320d9
activating narrowing-based quickcheck by default
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Aug 18 16:52:19 2011 +0900
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Aug 18 12:06:17 2011 +0200
     1.3 @@ -465,7 +465,7 @@
     1.4  
     1.5  (* setup *)
     1.6  
     1.7 -val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
     1.8 +val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
     1.9  
    1.10  val setup =
    1.11    Code.datatype_interpretation ensure_partial_term_of
    1.12 @@ -474,4 +474,4 @@
    1.13      (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
    1.14    #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
    1.15      
    1.16 -end;
    1.17 \ No newline at end of file
    1.18 +end;