--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Mar 28 10:25:28 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Mar 28 17:33:16 2011 +0200
@@ -159,7 +159,7 @@
by (rule Rep_Nat_inverse)
lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
+nitpick [card = 1, unary_ints, max_potential = 0, timeout = 120, expect = none]
by (rule Zero_int_def_raw)
lemma "Abs_list (Rep_list a) = a"
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Mar 28 10:25:28 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Mar 28 17:33:16 2011 +0200
@@ -50,8 +50,8 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-(*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]*)
-quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
+(*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 600.0, expect = no_counterexample]*)
+quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 600.0, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Mar 28 10:25:28 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Mar 28 17:33:16 2011 +0200
@@ -2,6 +2,8 @@
imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
begin
+declare [[values_timeout = 240.0]]
+
subsection {* Basic predicates *}
inductive False' :: "bool"
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Mar 28 10:25:28 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Mar 28 17:33:16 2011 +0200
@@ -2,6 +2,8 @@
imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
begin
+declare [[values_timeout = 240.0]]
+
section {* Specialisation Examples *}
primrec nth_el'