changeset 45451 | 74515e8e6046 |
parent 43686 | bc7d63c7fd6f |
child 58249 | 180f1b3508ed |
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Nov 11 08:32:45 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Nov 11 08:32:48 2011 +0100 @@ -29,7 +29,7 @@ lemma "exec c s s' ==> exec (Seq c c) s s'" -quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample] +quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample] oops