1.1 --- a/src/HOL/Fun.thy	Sun Jul 17 22:24:08 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sun Jul 17 22:25:14 2011 +0200
     1.3 @@ -34,15 +34,9 @@
     1.4  lemma id_apply [simp]: "id x = x"
     1.5    by (simp add: id_def)
     1.6  
     1.7 -lemma image_ident [simp]: "(%x. x) ` Y = Y"
     1.8 -by blast
     1.9 -
    1.10  lemma image_id [simp]: "id ` Y = Y"
    1.11  by (simp add: id_def)
    1.12  
    1.13 -lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
    1.14 -by blast
    1.15 -
    1.16  lemma vimage_id [simp]: "id -` A = A"
    1.17  by (simp add: id_def)
    1.18