src/ZF/AC/AC_Equiv.ML

--- a/src/ZF/AC/AC_Equiv.ML	Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Thu Aug 06 10:38:57 1998 +0200
@@ -118,10 +118,6 @@
         addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
 qed "inj_strengthen_type";
 
-Goal "A*B=0 <-> A=0 | B=0";
-by (fast_tac (claset() addSIs [equals0I] addEs [equals0E]) 1);
-qed "Sigma_empty_iff";
-
 Goalw [Finite_def] "n:nat ==> Finite(n)";
 by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
 qed "nat_into_Finite";