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.
raised timeout further, for SML/NJ
authorkrauss
Thu, 07 Apr 2011 21:49:24 +0200
changeset 42291 682b35dc1926
parent 42276 992892b48296
child 42292 b3196458428b
child 42304 34366f39d32d
raised timeout further, for SML/NJ
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	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
isabelle