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 *}