1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -41,12 +41,19 @@
     1.4  
     1.5  end
     1.6  
     1.7 -setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
     1.8 -  Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
     1.9 +ML {* 
    1.10 +val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false);
    1.11 +val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false);
    1.12 +*}
    1.13  
    1.14 -
    1.15 -setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
    1.16 -  Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
    1.17 +setup {*
    1.18 +  Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14",
    1.19 +    (small_14_active, Predicate_Compile_Quickcheck.test_goals
    1.20 +      (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14))))
    1.21 +  #> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15",
    1.22 +    (small_15_active, Predicate_Compile_Quickcheck.test_goals
    1.23 +      (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15))))
    1.24 +*}
    1.25  
    1.26  lemma
    1.27    "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"

     2.1 --- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Mon Jul 18 10:34:21 2011 +0200
     2.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Mon Jul 18 10:34:21 2011 +0200
     2.3 @@ -18,6 +18,8 @@
     2.4    inf (infixl "\<sqinter>" 70) and
     2.5    sup (infixl "\<squnion>" 65)
     2.6  
     2.7 +declare [[quickcheck_narrowing_active = false]]
     2.8 +
     2.9  subsection {* Distributive lattices *}
    2.10  
    2.11  lemma sup_inf_distrib2: