# HG changeset patch # User bulwahn # Date 1328174170 -3600 # Node ID eef663f8242e66ae7d41174de7efa52531cda777 # Parent da32cf32c0c799bf5f9d575bae1f0d6e58f9e22a adding an example for finite and cofinite sets diff -r da32cf32c0c7 -r eef663f8242e src/HOL/ex/Quickcheck_Examples.thy --- a/src/HOL/ex/Quickcheck_Examples.thy Thu Feb 02 10:12:30 2012 +0100 +++ b/src/HOL/ex/Quickcheck_Examples.thy Thu Feb 02 10:16:10 2012 +0100 @@ -267,6 +267,14 @@ oops +subsection {* Examples with sets *} + +lemma + "{} = A Un - A" +quickcheck[exhaustive, expect = counterexample] +oops + + subsection {* Examples with relations *} lemma