# HG changeset patch
# User oheimb
# Date 878673035 -3600
# Node ID 4830f1f5f6eae492a1e09186f6c206951aff132f
# Parent  5c6cb2a258169d0fd944cda2a87eb8fbb7d00e0e
removed redundant ball_empty and bex_empty (see equalities.ML)

diff -r 5c6cb2a25816 -r 4830f1f5f6ea src/HOL/Set.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";