Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generalizing inj_on_Int
authorbulwahn
Wed, 22 Feb 2012 08:05:28 +0100
changeset 46586 abbec6fa25c8
parent 46585 f462e49eaf11
child 46587 d3bcc356cc60
generalizing inj_on_Int
src/HOL/Fun.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle