# HG changeset patch
# User paulson
# Date 902393233 -7200
# Node ID 1d11c7e4b99949b167c03bcf4d4bb2c76f0ec0ae
# Parent  9d1d4c43c76d8fee5af6f8a76cd78f25b3c0c80c
Now recognizes both {}= and ={}

diff -r 9d1d4c43c76d -r 1d11c7e4b999 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Aug 06 10:38:57 1998 +0200
+++ b/src/HOL/Set.ML	Thu Aug 06 10:47:13 1998 +0200
@@ -263,7 +263,7 @@
 qed_goal "equals0E" Set.thy "!!a. [| A={};  a:A |] ==> P"
  (fn _ => [ (Blast_tac 1) ]);
 
-AddEs [equals0E];
+AddEs [equals0E, sym RS equals0E];
 
 Goalw [Ball_def] "Ball {} P = True";
 by (Simp_tac 1);