--- a/src/HOL/ex/Quickcheck_Examples.thy Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy Wed Mar 30 09:44:16 2011 +0200
@@ -50,9 +50,14 @@
oops
theorem "rev xs = xs"
- quickcheck[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
- oops
+ quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
+ quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
+ quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
+ quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
+ quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
+ quickcheck[tester = exhaustive, finite_types = false, expect = counterexample]
+oops
+
text {* An example involving functions inside other data structures *}