# HG changeset patch
# User wenzelm
# Date 963522612 -7200
# Node ID a93a7b6bb654b04429071b029d63b4bce5a88841
# Parent  ab5b24cbaa16bd93d424911305baba3f1791a11d
fixed name: UN_empty3;

diff -r ab5b24cbaa16 -r a93a7b6bb654 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Jul 13 23:09:25 2000 +0200
+++ b/src/HOL/equalities.ML	Thu Jul 13 23:10:12 2000 +0200
@@ -592,8 +592,8 @@
 
 Goal "(UNION A B = {}) = (ALL x:A. B x = {})";
 by Auto_tac; 
-qed "UN_empty";
-AddIffs [UN_empty];
+qed "UN_empty3";
+AddIffs [UN_empty3];
 
 
 (*Distributive laws...*)