src/HOL/Set.ML

   [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]);
 
 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";
 
 qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)"
  (fn _ => [ (Asm_simp_tac 1) ]);