# HG changeset patch
# User paulson
# Date 865585333 -7200
# Node ID 16ae2c20801cf56d415b63e6b952b9d0dba1a341
# Parent  be777156c7e98052c86765dfdadd03490009fb96
New miniscoping rules for ALL

diff -r be777156c7e9 -r 16ae2c20801c src/HOL/equalities.ML
--- 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)",