# HG changeset patch
# User nipkow
# Date 985603874 -7200
# Node ID fef9da0ee890caf2a40147927e61766ebe318e4d
# Parent  72c5997e11451ca27ebc9be1076032a3ed779b47
I forgot a few bases cases for the 1-point rules...

diff -r 72c5997e1145 -r fef9da0ee890 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Mar 23 12:10:05 2001 +0100
+++ b/src/HOL/Set.ML	Mon Mar 26 12:51:14 2001 +0200
@@ -100,15 +100,28 @@
 
 Addsimps [ball_triv, bex_triv];
 
-Goalw [Bex_def] "(ALL x:A. x=a --> P x) = (a:A --> P a)";
+Goal "(EX x:A. x=a) = (a:A)";
 by(Blast_tac 1);
-qed "ball_one_point";
+qed "bex_triv_one_point1";
+
+Goal "(EX x:A. a=x) = (a:A)";
+by(Blast_tac 1);
+qed "bex_triv_one_point2";
 
 Goal "(EX x:A. x=a & P x) = (a:A & P a)";
 by(Blast_tac 1);
-qed "bex_one_point";
+qed "bex_one_point1";
+
+Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)";
+by(Blast_tac 1);
+qed "ball_one_point1";
 
-Addsimps [ball_one_point,bex_one_point];
+Goal "(ALL x:A. a=x --> P x) = (a:A --> P a)";
+by(Blast_tac 1);
+qed "ball_one_point2";
+
+Addsimps [bex_triv_one_point1,bex_triv_one_point2,bex_one_point1,
+          ball_one_point1,ball_one_point2];
 
 let
 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))