Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT

1.1 --- a/src/HOL/Set.ML Fri Jun 16 13:15:04 2000 +0200
1.2 +++ b/src/HOL/Set.ML Fri Jun 16 13:15:40 2000 +0200
1.3 @@ -212,10 +212,7 @@
1.4 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
1.5 qed "equalityE";
1.6
1.7 -(*This could be tried. Most things build fine with it. However, some proofs
1.8 - become very slow or even fail.
1.9 - AddEs [equalityE];
1.10 -*)
1.11 +AddEs [equalityE];
1.12
1.13 val major::prems = Goal
1.14 "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P";
1.15 @@ -295,9 +292,6 @@
1.16 by (Blast_tac 1) ;
1.17 qed "equals0D";
1.18
1.19 -(* [| A = {}; a : A |] ==> R *)
1.20 -AddDs [equals0D, sym RS equals0D];
1.21 -
1.22 Goalw [Ball_def] "Ball {} P = True";
1.23 by (Simp_tac 1);
1.24 qed "ball_empty";