# HG changeset patch
# User bulwahn
# Date 1327575845 -3600
# Node ID 54227223a8d481aef76c8ab1e6173d360593b7df
# Parent  39fe503602fba638bc1948091b038421985c6375
adding quickcheck example with THE

diff -r 39fe503602fb -r 54227223a8d4 src/HOL/ex/Quickcheck_Examples.thy
--- 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