1.1 --- a/src/HOL/Set.ML	Tue Nov 04 20:49:45 1997 +0100
     1.2 +++ b/src/HOL/Set.ML	Tue Nov 04 20:50:35 1997 +0100
     1.3 @@ -233,15 +233,6 @@
     1.4  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
     1.5   (fn _ => [ (Blast_tac 1) ]);
     1.6  
     1.7 -goal Set.thy "Ball {} P = True";
     1.8 -by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1);
     1.9 -qed "ball_empty";
    1.10 -
    1.11 -goal Set.thy "Bex {} P = False";
    1.12 -by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Bex_def, empty_def]) 1);
    1.13 -qed "bex_empty";
    1.14 -Addsimps [ball_empty, bex_empty];
    1.15 -
    1.16  
    1.17  section "The Powerset operator -- Pow";
    1.18