# HG changeset patch
# User berghofe
# Date 1120219073 -7200
# Node ID 1ed737a98198b3419404d2b9f804ebc571ffff6f
# Parent  bf7de5723c60297d180fc49b570ecd229692fd17
Added strong_ball_cong and strong_bex_cong (these are now the standard
congruence rules for Ball and Bex).

diff -r bf7de5723c60 -r 1ed737a98198 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Jul 01 13:56:34 2005 +0200
+++ b/src/HOL/Set.thy	Fri Jul 01 13:57:53 2005 +0200
@@ -444,16 +444,26 @@
 
 subsubsection {* Congruence rules *}
 
-lemma ball_cong [cong]:
+lemma ball_cong:
   "A = B ==> (!!x. x:B ==> P x = Q x) ==>
     (ALL x:A. P x) = (ALL x:B. Q x)"
   by (simp add: Ball_def)
 
-lemma bex_cong [cong]:
+lemma strong_ball_cong [cong]:
+  "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>
+    (ALL x:A. P x) = (ALL x:B. Q x)"
+  by (simp add: simp_implies_def Ball_def)
+
+lemma bex_cong:
   "A = B ==> (!!x. x:B ==> P x = Q x) ==>
     (EX x:A. P x) = (EX x:B. Q x)"
   by (simp add: Bex_def cong: conj_cong)
 
+lemma strong_bex_cong [cong]:
+  "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>
+    (EX x:A. P x) = (EX x:B. Q x)"
+  by (simp add: simp_implies_def Bex_def cong: conj_cong)
+
 
 subsubsection {* Subsets *}