# HG changeset patch
# User paulson
# Date 905441916 -7200
# Node ID f864dbcda5f1c53e64f44b8db2aeef3a7e6cfb9e
# Parent  2ea5d254e44e2a268256690bc5abf854fb5b52a2
deleted the bogus equals0E, fixed equals0D

diff -r 2ea5d254e44e -r f864dbcda5f1 src/ZF/ZF.ML
--- 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 ]);