author | haftmann |
Sun, 17 Jul 2011 22:25:14 +0200 | |
changeset 43874 | 74f1f2dd8f52 |
parent 43873 | 8a2f339641c1 |
child 43875 | 485d2ad43528 |
src/HOL/Fun.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Fun.thy Sun Jul 17 22:24:08 2011 +0200 +++ b/src/HOL/Fun.thy Sun Jul 17 22:25:14 2011 +0200 @@ -34,15 +34,9 @@ lemma id_apply [simp]: "id x = x" by (simp add: id_def) -lemma image_ident [simp]: "(%x. x) ` Y = Y" -by blast - lemma image_id [simp]: "id ` Y = Y" by (simp add: id_def) -lemma vimage_ident [simp]: "(%x. x) -` Y = Y" -by blast - lemma vimage_id [simp]: "id -` A = A" by (simp add: id_def)