--- a/src/HOL/equalities.ML Wed Jun 21 10:31:34 2000 +0200
+++ b/src/HOL/equalities.ML Wed Jun 21 10:32:57 2000 +0200
@@ -366,7 +366,7 @@
Goal "(A Un B = {}) = (A = {} & B = {})";
by (blast_tac (claset() addEs [equalityCE]) 1);
qed "Un_empty";
-Addsimps[Un_empty];
+AddIffs[Un_empty];
Goal "(A Un B <= C) = (A <= C & B <= C)";
by (Blast_tac 1);
@@ -461,8 +461,8 @@
by (Blast_tac 1);
qed "Union_Int_subset";
-Goal "(Union M = {}) = (! A : M. A = {})";
-by (blast_tac (claset() addEs [equalityCE]) 1);
+Goal "(Union A = {}) = (ALL x:A. x={})";
+by Auto_tac;
qed "Union_empty_conv";
AddIffs [Union_empty_conv];
@@ -596,6 +596,11 @@
by (Blast_tac 1);
qed "INT_eq";
+Goal "(UNION A B = {}) = (ALL x:A. B x = {})";
+by Auto_tac;
+qed "UN_empty";
+AddIffs [UN_empty];
+
(*Distributive laws...*)