diff -r b7aa93c10833 -r 9eabcb1bfe50 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Mon Oct 25 21:17:11 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Mon Oct 25 21:17:12 2010 +0200 @@ -23,7 +23,7 @@ setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} lemma "\ hotel s; g \ isin s r \ \ owns s r = Some g" -quickcheck[generator = code, iterations = 100000, report] +quickcheck[generator = code, iterations = 10000, report] quickcheck[generator = prolog, iterations = 1, expect = counterexample] oops