# HG changeset patch # User bulwahn # Date 1309953472 -7200 # Node ID 2882832b8d890251b84d8a1270c4514dbde26ba4 # Parent ff935aea9557aa9f83b87d8242017b6ff20caea9# Parent bc7d63c7fd6f27a98b9decd9b3912286ff070b0d merged diff -r ff935aea9557 -r 2882832b8d89 src/HOL/Predicate_Compile_Examples/IMP_1.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Wed Jul 06 09:54:40 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Wed Jul 06 13:57:52 2011 +0200 @@ -26,7 +26,7 @@ lemma "exec c s s' ==> exec (Seq c c) s s'" -quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, timeout = 600.0, expect = counterexample] +quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample] oops diff -r ff935aea9557 -r 2882832b8d89 src/HOL/Predicate_Compile_Examples/IMP_2.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Wed Jul 06 09:54:40 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Wed Jul 06 13:57:52 2011 +0200 @@ -29,7 +29,7 @@ lemma "exec c s s' ==> exec (Seq c c) s s'" -quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, timeout = 600.0, expect = counterexample] +quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample] oops diff -r ff935aea9557 -r 2882832b8d89 src/HOL/Predicate_Compile_Examples/IMP_3.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Wed Jul 06 09:54:40 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Wed Jul 06 13:57:52 2011 +0200 @@ -29,8 +29,8 @@ lemma "exec c s s' ==> exec (Seq c c) s s'" - quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample] + quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=100, quiet = false, expect = counterexample] oops -end \ No newline at end of file +end diff -r ff935aea9557 -r 2882832b8d89 src/HOL/Predicate_Compile_Examples/IMP_4.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy Wed Jul 06 09:54:40 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Wed Jul 06 13:57:52 2011 +0200 @@ -30,7 +30,7 @@ lemma "exec c s s' ==> exec (Seq c c) s s'" nitpick (* nitpick fails here! *) - quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample] + quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=100, expect=counterexample] oops -end \ No newline at end of file +end diff -r ff935aea9557 -r 2882832b8d89 src/HOL/ex/SML_Quickcheck_Examples.thy --- a/src/HOL/ex/SML_Quickcheck_Examples.thy Wed Jul 06 09:54:40 2011 +0200 +++ b/src/HOL/ex/SML_Quickcheck_Examples.thy Wed Jul 06 13:57:52 2011 +0200 @@ -16,6 +16,7 @@ *} declare [[quickcheck_finite_types = false]] +declare [[quickcheck_timeout = 600.0]] subsection {* Lists *} @@ -139,4 +140,4 @@ --{* Wrong! *} oops -end \ No newline at end of file +end