changeset 46337 | 54227223a8d4 |
parent 46169 | 321abd584588 |
child 46344 | b6fbdd3d0915 |
--- a/src/HOL/ex/Quickcheck_Examples.thy Thu Jan 26 12:03:35 2012 +0100 +++ b/src/HOL/ex/Quickcheck_Examples.thy Thu Jan 26 12:04:05 2012 +0100 @@ -279,6 +279,14 @@ (* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *) oops +subsection {* Examples with the descriptive operator *} + +lemma + "(THE x. x = a) = b" +quickcheck[random, expect = counterexample] +quickcheck[exhaustive, expect = counterexample] +oops + subsection {* Examples with Multisets *} lemma