src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
changeset 42397 13798dcbdca5
parent 42291 682b35dc1926
child 43888 ee4be704c2a4
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Apr 18 16:33:45 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Apr 18 17:07:47 2011 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  lemma
     1.5    "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
     1.6  (*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*)
     1.7 -quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = counterexample]
     1.8 +quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample]
     1.9  oops
    1.10  
    1.11