# HG changeset patch
# User paulson
# Date 961154140 -7200
# Node ID e8521ed7f35ba1879173a01d0b02b4d1aa1ad6e9
# Parent  2313ddc415a199c2fd7c8ffb1b285dc8eb4a6947
Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT

diff -r 2313ddc415a1 -r e8521ed7f35b src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Jun 16 13:15:04 2000 +0200
+++ b/src/HOL/Set.ML	Fri Jun 16 13:15:40 2000 +0200
@@ -212,10 +212,7 @@
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 qed "equalityE";
 
-(*This could be tried.  Most things build fine with it.  However, some proofs
-  become very slow or even fail.
-  AddEs [equalityE];
-*)
+AddEs [equalityE];
 
 val major::prems = Goal
     "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
@@ -295,9 +292,6 @@
 by (Blast_tac 1) ;
 qed "equals0D";
 
-(* [| A = {};  a : A |] ==> R *)
-AddDs [equals0D, sym RS equals0D];
-
 Goalw [Ball_def] "Ball {} P = True";
 by (Simp_tac 1);
 qed "ball_empty";