src/ZF/ZF.ML

--- a/src/ZF/ZF.ML	Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/ZF.ML	Thu Aug 06 10:38:57 1998 +0200
@@ -447,6 +447,8 @@
 qed_goal "equals0E" ZF.thy "!!P. [| A=0;  a:A |] ==> P"
  (fn _=> [ Full_simp_tac 1, Blast_tac 1 ]);
 
+AddEs [equals0E, sym RS equals0E];
+
 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
  (fn _=> [ Blast_tac 1 ]);