diff -r f7a573c46611 -r 60613b065e9b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed May 22 17:11:54 1996 +0200
+++ b/src/HOL/simpdata.ML	Wed May 22 17:30:16 1996 +0200
@@ -192,6 +192,8 @@
 prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
 
+prove "ex_imp" "((? x. P x) --> Q) = (!x. P x --> Q)";
+
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);