# HG changeset patch
# User paulson
# Date 905440849 -7200
# Node ID fe9d103464a4b48b292b69ce47a9f154805e19d4
# Parent  d853d1ac85a35503c1e57219a5045c382985eed3
Changed equals0E back to equals0D and gave it the correct destruct form

diff -r d853d1ac85a3 -r fe9d103464a4 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Sep 10 17:17:22 1998 +0200
+++ b/src/HOL/Set.ML	Thu Sep 10 17:20:49 1998 +0200
@@ -115,8 +115,6 @@
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
 qed "subsetI";
 
-Blast.overloaded ("op <=", domain_type); (*The <= relation is overloaded*)
-
 (*While (:) is not, its type must be kept
   for overloading of = to work.*)
 Blast.overloaded ("op :", domain_type);
@@ -257,10 +255,10 @@
   [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]);
 
 (*Use for reasoning about disjointness: A Int B = {} *)
-qed_goal "equals0E" Set.thy "!!a. [| A={};  a:A |] ==> P"
+qed_goal "equals0D" Set.thy "!!a. A={} ==> a ~: A"
  (fn _ => [ (Blast_tac 1) ]);
 
-AddEs [equals0E, sym RS equals0E];
+AddDs [equals0D, sym RS equals0D];
 
 Goalw [Ball_def] "Ball {} P = True";
 by (Simp_tac 1);