author | paulson |
Tue, 08 May 2001 16:01:36 +0200 | |
changeset 11290 | c6a4100d1cd0 |
parent 11289 | 65782388cf40 |
child 11291 | 02db0084a695 |
src/HOL/Set.ML | file | annotate | diff | comparison | revisions |
--- 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";