src/HOL/Set.ML

 by (simp_tac (simpset() addsimps [Bex_def]) 1);
 qed "bex_triv";
 
 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";
 
 Goal "(EX x:A. a=x) = (a:A)";

 
 Goal "(EX x:A. x=a & P x) = (a:A & P a)";
 by(Blast_tac 1);
 qed "bex_one_point1";
 
+Goal "(EX x:A. a=x & P x) = (a:A & P a)";
+by(Blast_tac 1);
+qed "bex_one_point2";
+
 Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)";
 by(Blast_tac 1);
 qed "ball_one_point1";
 
 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,
+Addsimps [bex_triv_one_point1,bex_triv_one_point2,
+          bex_one_point1,bex_one_point2,
           ball_one_point1,ball_one_point2];
 
 let
 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
     ("EX x:A. P(x) & Q(x)",HOLogic.boolT)

                     Quantifier1.prove_one_point_ex_tac;
 
 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
-    ("ALL x:A. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
-
-val swap = prove_goal thy
-  "((!x. A x & EP x --> Q x) = (!x. E x --> A x & P x --> Q x)) ==> \
-\  ((!x. A x --> EP x --> Q x) = (!x. A x --> E x --> P x --> Q x))"
-  (fn ths => [cut_facts_tac ths 1, Blast_tac 1]);
-
-val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN rtac swap 1 THEN
+    ("ALL x:A. P(x) --> Q(x)",HOLogic.boolT)
+
+val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN
                      Quantifier1.prove_one_point_all_tac;
 
 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
 
 val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;