1.1 --- a/src/HOL/Set.ML	Thu Sep 10 17:17:22 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Sep 10 17:20:49 1998 +0200
     1.3 @@ -115,8 +115,6 @@
     1.4  by (REPEAT (ares_tac (prems @ [ballI]) 1));
     1.5  qed "subsetI";
     1.6  
     1.7 -Blast.overloaded ("op <=", domain_type); (*The <= relation is overloaded*)
     1.8 -
     1.9  (*While (:) is not, its type must be kept
    1.10    for overloading of = to work.*)
    1.11  Blast.overloaded ("op :", domain_type);
    1.12 @@ -257,10 +255,10 @@
    1.13    [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]);
    1.14  
    1.15  (*Use for reasoning about disjointness: A Int B = {} *)
    1.16 -qed_goal "equals0E" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.17 +qed_goal "equals0D" Set.thy "!!a. A={} ==> a ~: A"
    1.18   (fn _ => [ (Blast_tac 1) ]);
    1.19  
    1.20 -AddEs [equals0E, sym RS equals0E];
    1.21 +AddDs [equals0D, sym RS equals0D];
    1.22  
    1.23  Goalw [Ball_def] "Ball {} P = True";
    1.24  by (Simp_tac 1);