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);