# HG changeset patch
# User krauss
# Date 1301326396 -7200
# Node ID d24a93025feb7c4440bdb6e067c87bd1777fc016
# Parent  2c255ba8f299e91739d86ee9cbbbe21731762dd0
raised various timeouts to accommodate sluggish SML/NJ

diff -r 2c255ba8f299 -r d24a93025feb src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- 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"
diff -r 2c255ba8f299 -r d24a93025feb src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
--- 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
 
 
diff -r 2c255ba8f299 -r d24a93025feb src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- 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"
diff -r 2c255ba8f299 -r d24a93025feb src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- 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'