src/HOL/BNF_FP_Base.thy
changeset 55930 25a90cebbbe5
parent 55906 abf91ebd0820
child 55931 62156e694f3d
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Mar 05 17:23:28 2014 -0800
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 12:17:26 2014 +0100
     1.3 @@ -98,13 +98,6 @@
     1.4  "setr (Inr x) = {x}"
     1.5  unfolding sum_set_defs by simp+
     1.6  
     1.7 -lemma UN_compreh_eq_eq:
     1.8 -"\<Union>{y. y = A} = A"
     1.9 -by blast+
    1.10 -
    1.11 -lemma ex_in_single: "(\<exists>x \<in> {y}. P x) = P y"
    1.12 -by blast
    1.13 -
    1.14  lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
    1.15  by blast
    1.16