# HG changeset patch
# User haftmann
# Date 1310934314 -7200
# Node ID 74f1f2dd8f52d3273f5fb87ed69638b37d1f80bb
# Parent  8a2f339641c1060251abb8e62776b3587a48aecd
more on complement

diff -r 8a2f339641c1 -r 74f1f2dd8f52 src/HOL/Fun.thy
--- 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)