author | bulwahn |
Sun, 05 Feb 2012 08:57:03 +0100 | |
changeset 46421 | 5ab496224729 |
parent 46420 | 92b629f568c4 |
child 46422 | 23936fa78841 |
child 46423 | 51259911b9fa |
--- 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 *}