--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Jul 18 10:34:21 2011 +0200
@@ -41,12 +41,19 @@
end
-setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
- Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
+ML {*
+val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false);
+val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false);
+*}
-
-setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
- Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
+setup {*
+ Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14",
+ (small_14_active, Predicate_Compile_Quickcheck.test_goals
+ (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14))))
+ #> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15",
+ (small_15_active, Predicate_Compile_Quickcheck.test_goals
+ (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15))))
+*}
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
--- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy Mon Jul 18 10:34:21 2011 +0200
@@ -18,6 +18,8 @@
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65)
+declare [[quickcheck_narrowing_active = false]]
+
subsection {* Distributive lattices *}
lemma sup_inf_distrib2: