# HG changeset patch
# User nipkow
# Date 985690830 -7200
# Node ID d9bda7cbdf5665c359a9d9d660fec79d457a4826
# Parent  0adc5f9b4977d1090fb7e23e1685249c99cee0c6
fixed bug in tactic for ball 1 point simproc

diff -r 0adc5f9b4977 -r d9bda7cbdf56 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Mar 27 11:27:06 2001 +0200
+++ b/src/HOL/Set.ML	Tue Mar 27 13:00:30 2001 +0200
@@ -136,7 +136,8 @@
     ("ALL x:A. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
 
 val swap = prove_goal thy
-  "((!x. Q x --> P x --> R x) = S) ==> ((!x. P x --> Q x --> R x) = S)"
+  "((!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