# HG changeset patch
# User bulwahn
# Date 1329894328 -3600
# Node ID abbec6fa25c8e94d1c22e40641443d9b744f956d
# Parent  f462e49eaf115a27f8ac058f0f094e8c46c51e37
generalizing inj_on_Int

diff -r f462e49eaf11 -r abbec6fa25c8 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Feb 22 08:01:41 2012 +0100
+++ b/src/HOL/Fun.thy	Wed Feb 22 08:05:28 2012 +0100
@@ -166,7 +166,7 @@
 lemma inj_on_id2[simp]: "inj_on (%x. x) A"
 by (simp add: inj_on_def)
 
-lemma inj_on_Int: "\<lbrakk>inj_on f A; inj_on f B\<rbrakk> \<Longrightarrow> inj_on f (A \<inter> B)"
+lemma inj_on_Int: "inj_on f A \<or> inj_on f B \<Longrightarrow> inj_on f (A \<inter> B)"
 unfolding inj_on_def by blast
 
 lemma inj_on_INTER: