--- a/src/ZF/ZF.ML Thu Sep 10 17:36:42 1998 +0200
+++ b/src/ZF/ZF.ML Thu Sep 10 17:38:36 1998 +0200
@@ -444,10 +444,10 @@
qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
(fn prems=> [ blast_tac (claset() addDs prems) 1 ]);
-qed_goal "equals0E" ZF.thy "!!P. [| A=0; a:A |] ==> P"
- (fn _=> [ Full_simp_tac 1, Blast_tac 1 ]);
+qed_goal "equals0D" ZF.thy "!!P. A=0 ==> a ~: A"
+ (fn _=> [ Blast_tac 1 ]);
-AddEs [equals0E, sym RS equals0E];
+AddDs [equals0D, sym RS equals0D];
qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
(fn _=> [ Blast_tac 1 ]);