adding a remark about lemma which is too special and should be removed
authorbulwahn
Sun, 05 Feb 2012 08:36:41 +0100
changeset 46419 e139d0e29ca1
parent 46418 22bb415d7754
child 46420 92b629f568c4
adding a remark about lemma which is too special and should be removed
src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Feb 05 08:24:39 2012 +0100
+++ b/src/HOL/Fun.thy	Sun Feb 05 08:36:41 2012 +0100
@@ -427,6 +427,7 @@
   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'"