src/HOL/ex/Quickcheck_Examples.thy
changeset 46421 5ab496224729
parent 46397 eef663f8242e
--- a/src/HOL/ex/Quickcheck_Examples.thy	Sun Feb 05 08:47:13 2012 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Sun Feb 05 08:57:03 2012 +0100
@@ -274,6 +274,11 @@
 quickcheck[exhaustive, expect = counterexample]
 oops
 
+lemma
+  "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
 
 subsection {* Examples with relations *}