src/ZF/equalities.ML

--- a/src/ZF/equalities.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/equalities.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -200,6 +200,10 @@
 by (fast_tac eq_cs 1);
 val Inter_eq_INT = result();
 
+goal ZF.thy "(UN i:0. A(i)) = 0";
+by (fast_tac eq_cs 1);
+val UN_0 = result();
+
 (*Halmos, Naive Set Theory, page 35.*)
 goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
 by (fast_tac eq_cs 1);