diff -r 6c9453ec2191 -r 74f1b0f10b2b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Set.thy	Sun Oct 21 09:39:09 2018 +0200
@@ -422,24 +422,24 @@
 text \<open>Congruence rules\<close>
 
 lemma ball_cong:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+  "\<lbrakk> A = B;  \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
-  by (simp add: Ball_def)
-
-lemma strong_ball_cong [cong]:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+by (simp add: Ball_def)
+
+lemma ball_cong_strong [cong]:
+  "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
-  by (simp add: simp_implies_def Ball_def)
+by (simp add: simp_implies_def Ball_def)
 
 lemma bex_cong:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+  "\<lbrakk> A = B;  \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
-  by (simp add: Bex_def cong: conj_cong)
-
-lemma strong_bex_cong [cong]:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+by (simp add: Bex_def cong: conj_cong)
+
+lemma bex_cong_strong [cong]:
+  "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
-  by (simp add: simp_implies_def Bex_def cong: conj_cong)
+by (simp add: simp_implies_def Bex_def cong: conj_cong)
 
 lemma bex1_def: "(\<exists>!x\<in>X. P x) \<longleftrightarrow> (\<exists>x\<in>X. P x) \<and> (\<forall>x\<in>X. \<forall>y\<in>X. P x \<longrightarrow> P y \<longrightarrow> x = y)"
   by auto