1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 14 22:23:11 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 14 22:23:11 2012 +0200
     1.3 @@ -104,6 +104,7 @@
     1.4  "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
     1.5  by simp
     1.6  
     1.7 +(* TODO: cleanup *)
     1.8  lemma UN_compreh_bex:
     1.9  "\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
    1.10  "\<Union>{y. \<exists>x \<in> A. y = {x}} = A"