Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generous timeout gives more breath in parallel run on less luxury machines
authorhaftmann
Mon, 22 Nov 2010 14:27:42 +0100
changeset 40661 f643399acab3
parent 40660 86a1f61d260e
child 40662 798aad2229c0
child 40673 3b9b39ac1f24
child 40674 54dbe6a1c349
generous timeout gives more breath in parallel run on less luxury machines
src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 14:19:03 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 14:27:42 2010 +0100
@@ -50,8 +50,8 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample]
-quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample]
+quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
+quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
 oops
isabelle