# HG changeset patch
# User bulwahn
# Date 1328428033 -3600
# Node ID 92b629f568c4786bd5c0e42348309367998a8ecb
# Parent  e139d0e29ca11426f1c5086579520bf1d4cba871
removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)

diff -r e139d0e29ca1 -r 92b629f568c4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Feb 05 08:36:41 2012 +0100
+++ b/src/HOL/Fun.thy	Sun Feb 05 08:47:13 2012 +0100
@@ -427,28 +427,6 @@
   using * by blast
 qed
 
-(* FIXME: bij_betw_Disj_Un is special case of bij_betw_combine -- should be removed *)
-lemma bij_betw_Disj_Un:
-  assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
-          B1: "bij_betw f A A'" and B2: "bij_betw f B B'"
-  shows "bij_betw f (A \<union> B) (A' \<union> B')"
-proof-
-  have 1: "inj_on f A \<and> inj_on f B"
-  using B1 B2 by (auto simp add: bij_betw_def)
-  have 2: "f`A = A' \<and> f`B = B'"
-  using B1 B2 by (auto simp add: bij_betw_def)
-  hence "f`(A - B) \<inter> f`(B - A) = {}"
-  using DISJ DISJ' by blast
-  hence "inj_on f (A \<union> B)"
-  using 1 by (auto simp add: inj_on_Un)
-  (*  *)
-  moreover
-  have "f`(A \<union> B) = A' \<union> B'"
-  using 2 by auto
-  ultimately show ?thesis
-  unfolding bij_betw_def by auto
-qed
-
 lemma bij_betw_subset:
   assumes BIJ: "bij_betw f A A'" and
           SUB: "B \<le> A" and IM: "f ` B = B'"