# 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