AddIffs [all_not_in_conv];

--- 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());