# HG changeset patch
# User paulson
# Date 853514251 -3600
# Node ID 761e3094e32f06e243d07499b0c33bad6f3a3867
# Parent  bee082efaa4608e8260a1f6444d150649da72da5
New rewrites for bounded quantifiers

diff -r bee082efaa46 -r 761e3094e32f src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jan 17 13:21:54 1997 +0100
+++ b/src/HOL/equalities.ML	Fri Jan 17 16:17:31 1997 +0100
@@ -458,13 +458,16 @@
 
 section"Bounded quantifiers";
 
-goal Set.thy "(!x:insert a A.P x) = (P a & (!x:A.P x))";
-by (Fast_tac 1);
-qed "Ball_insert";
+(** These are not added to the default simpset because (a) they duplicate the
+    body and (b) there are no similar rules for Int. **)
 
-goal Set.thy "(!x:A Un B.P x) = ((!x:A.P x) & (!x:B.P x))";
+goal Set.thy "(ALL x:A Un B.P x) = ((ALL x:A.P x) & (ALL x:B.P x))";
 by (Fast_tac 1);
-qed "Ball_Un";
+qed "ball_Un";
+
+goal Set.thy "(EX x:A Un B.P x) = ((EX x:A.P x) | (EX x:B.P x))";
+by (Fast_tac 1);
+qed "bex_Un";
 
 
 section "-";