New miniscoping rules for ALL

--- a/src/HOL/equalities.ML	Fri Jun 06 10:21:10 1997 +0200
+++ b/src/HOL/equalities.ML	Fri Jun 06 10:22:13 1997 +0200
@@ -681,6 +681,8 @@
 val ball_simps = map prover
     ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
      "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
+     "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
+     "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
      "(ALL x:{}. P x) = True",
      "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
      "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",