| changeset 43874 | 74f1f2dd8f52 |
| parent 43705 | 8e421a529a48 |
| child 43991 | f4a7697011c5 |
--- 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)