removed redundant ball_empty and bex_empty (see equalities.ML)

--- a/src/HOL/Set.ML	Tue Nov 04 20:49:45 1997 +0100
+++ b/src/HOL/Set.ML	Tue Nov 04 20:50:35 1997 +0100
@@ -233,15 +233,6 @@
 qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
  (fn _ => [ (Blast_tac 1) ]);
 
-goal Set.thy "Ball {} P = True";
-by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1);
-qed "ball_empty";
-
-goal Set.thy "Bex {} P = False";
-by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Bex_def, empty_def]) 1);
-qed "bex_empty";
-Addsimps [ball_empty, bex_empty];
-
 
 section "The Powerset operator -- Pow";