1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Sat Sep 15 20:14:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Sat Sep 15 21:10:26 2012 +0200
     1.3 @@ -104,10 +104,8 @@
     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"
    1.11  "\<Union>{y. \<exists>x \<in> A. y = {f x}} = {y. \<exists>x \<in> A. y = f x}"
    1.12  by blast+
    1.13