src/ZF/AC/AC7_AC9.ML
changeset 5470 855654b691db
parent 5325 f7a5e06adea1
child 9683 f87c8c449018
--- a/src/ZF/AC/AC7_AC9.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC7_AC9.ML	Thu Sep 10 17:42:44 1998 +0200
@@ -91,8 +91,7 @@
 val lemma1_2 = result();
 
 Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 ==> (PROD B:A. B) ~= 0";
-by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]
-                addSEs [equals0E]) 1);
+by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]) 1);
 val lemma1 = result();
 
 Goal "0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";