# HG changeset patch
# User paulson
# Date 989330496 -7200
# Node ID c6a4100d1cd061961a866449e9579f4b7f695d32
# Parent  65782388cf40a11fa006637fbb1a360129a0dfcd
fixed comment

diff -r 65782388cf40 -r c6a4100d1cd0 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";