# HG changeset patch
# User nipkow
# Date 877709451 -7200
# Node ID 2bbeed529077b965b4e280e8ff3c5e3a9d706515
# Parent  6b8abfdf3ec47053d15ee138e4256b79efd3b35d
Added

goal Set.thy "(Union M = {}) = (! A : M. A = {})";
AddIffs [Union_empty_conv];

Good idea??

diff -r 6b8abfdf3ec4 -r 2bbeed529077 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Oct 24 18:02:23 1997 +0200
+++ b/src/HOL/equalities.ML	Fri Oct 24 18:10:51 1997 +0200
@@ -336,6 +336,11 @@
 by (Blast_tac 1);
 qed "Union_Int_subset";
 
+goal Set.thy "(Union M = {}) = (! A : M. A = {})"; 
+by (blast_tac (!claset addEs [equalityE]) 1);
+qed"Union_empty_conv"; 
+AddIffs [Union_empty_conv];
+
 val prems = goal Set.thy
    "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
 by (blast_tac (!claset addSEs [equalityE]) 1);