# HG changeset patch
# User nipkow
# Date 877013671 -7200
# Node ID 51c00e87bd6edbb1350380d59d81bb3ef76eeb13
# Parent  5ae0e1324c563d169f0e268138af03dcc8cebccb
AddIffs [all_not_in_conv];

diff -r 5ae0e1324c56 -r 51c00e87bd6e src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Oct 16 15:33:06 1997 +0200
+++ b/src/HOL/equalities.ML	Thu Oct 16 16:54:31 1997 +0200
@@ -628,7 +628,7 @@
 goal Set.thy "(!x. x ~: A) = (A={})";
 by(Blast_tac 1);
 qed "all_not_in_conv";
-(* FIXME: AddIffs [all_not_in_conv]; *)
+AddIffs [all_not_in_conv];
 
 goalw Set.thy [Pow_def] "Pow {} = {{}}";
 by (Auto_tac());