src/HOL/equalities.ML
changeset 9312 a93a7b6bb654
parent 9206 eaaee6bd74ba
child 9338 fcf7f29a3447
--- 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...*)