# HG changeset patch
# User bulwahn
# Date 1328427401 -3600
# Node ID e139d0e29ca11426f1c5086579520bf1d4cba871
# Parent  22bb415d7754a365a45919505181030bf29a6e99
adding a remark about lemma which is too special and should be removed

diff -r 22bb415d7754 -r e139d0e29ca1 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'"