src/HOL/Fun.thy
changeset 47579 28f6f4ad69bf
parent 47488 be6dd389639d
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Fun.thy	Thu Apr 19 11:10:03 2012 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Apr 19 10:49:47 2012 +0200
     1.3 @@ -24,11 +24,11 @@
     1.4  lemma id_apply [simp]: "id x = x"
     1.5    by (simp add: id_def)
     1.6  
     1.7 -lemma image_id [simp]: "id ` Y = Y"
     1.8 -  by (simp add: id_def)
     1.9 +lemma image_id [simp]: "image id = id"
    1.10 +  by (simp add: id_def fun_eq_iff)
    1.11  
    1.12 -lemma vimage_id [simp]: "id -` A = A"
    1.13 -  by (simp add: id_def)
    1.14 +lemma vimage_id [simp]: "vimage id = id"
    1.15 +  by (simp add: id_def fun_eq_iff)
    1.16  
    1.17  
    1.18  subsection {* The Composition Operator @{text "f \<circ> g"} *}