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);