--- a/src/HOL/Set.thy Sat Oct 20 15:36:32 2018 +0200
+++ b/src/HOL/Set.thy Sun Oct 21 08:19:06 2018 +0200
@@ -936,8 +936,11 @@
"(\<lambda>x. if P x then f x else g x) ` S = f ` (S \<inter> {x. P x}) \<union> g ` (S \<inter> {x. \<not> P x})"
by auto
-lemma image_cong: "M = N \<Longrightarrow> (\<And>x. x \<in> N \<Longrightarrow> f x = g x) \<Longrightarrow> f ` M = g ` N"
- by (simp add: image_def)
+lemma image_cong: "\<lbrakk> M = N; \<And>x. x \<in> N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> f ` M = g ` N"
+by (simp add: image_def)
+
+lemma image_cong_strong: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
+by (simp add: image_def simp_implies_def)
lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
by blast