src/HOL/Fun.thy
changeset 46419 e139d0e29ca1
parent 45603 d2d9ef16ccaf
child 46420 92b629f568c4
     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'"