# HG changeset patch
# User krauss
# Date 1302205764 -7200
# Node ID 682b35dc1926d2b16b30a86286b33a5ec8123b31
# Parent  992892b482962a31d6a8e4368a0a5b70d819edbe
raised timeout further, for SML/NJ

diff -r 992892b48296 -r 682b35dc1926 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Thu Apr 07 18:41:49 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Thu Apr 07 21:49:24 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 = 600.0, expect = no_counterexample]*)
-quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 600.0, expect = counterexample]
+(*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*)
+quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = counterexample]
 oops