src/HOL/Set.ML

--- a/src/HOL/Set.ML	Tue May 08 16:01:28 2001 +0200
+++ b/src/HOL/Set.ML	Tue May 08 16:01:36 2001 +0200
@@ -100,17 +100,6 @@
 
 Addsimps [ball_triv, bex_triv];
 
-(* Blast cannot prove these (yet?).
-   Move somewhere else?
-Goal "(ALL x:A. x=a) = (A = {a})";
-by(Blast_tac 1);
-qed "ball_triv_one_point1";
-
-Goal "(ALL x:A. a=x) = (A = {a})";
-by(Blast_tac 1);
-qed "ball_triv_one_point2";
-*)
-
 Goal "(EX x:A. x=a) = (a:A)";
 by(Blast_tac 1);
 qed "bex_triv_one_point1";