# HG changeset patch
# User bulwahn
# Date 1328428623 -3600
# Node ID 5ab496224729fe1d0278f959e18e22ea1b16737c
# Parent  92b629f568c4786bd5c0e42348309367998a8ecb
adding a quickcheck example about functions and sets

diff -r 92b629f568c4 -r 5ab496224729 src/HOL/ex/Quickcheck_Examples.thy
--- 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 *}