# HG changeset patch
# User paulson
# Date 961576377 -7200
# Node ID 3a0912a127ec839758f667965dcb06a43a3b9469
# Parent  44cd0f9f8e5b0cff2c2b16f943362ba0dbcb3a29
new theorem UN_empty; it and Un_empty inserted by AddIffs

diff -r 44cd0f9f8e5b -r 3a0912a127ec src/HOL/equalities.ML
--- 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...*)