adding a remark about lemma which is too special and should be removed
authorbulwahn
Sun Feb 05 08:36:41 2012 +0100 (2012-02-05)
changeset 46419e139d0e29ca1
parent 46418 22bb415d7754
child 46420 92b629f568c4
adding a remark about lemma which is too special and should be removed
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Sun Feb 05 08:24:39 2012 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sun Feb 05 08:36:41 2012 +0100
     1.3 @@ -427,6 +427,7 @@
     1.4    using * by blast
     1.5  qed
     1.6  
     1.7 +(* FIXME: bij_betw_Disj_Un is special case of bij_betw_combine -- should be removed *)
     1.8  lemma bij_betw_Disj_Un:
     1.9    assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
    1.10            B1: "bij_betw f A A'" and B2: "bij_betw f B B'"