--- a/src/HOL/Fun.thy Thu Apr 19 11:10:03 2012 +0200
+++ b/src/HOL/Fun.thy Thu Apr 19 10:49:47 2012 +0200
@@ -24,11 +24,11 @@
lemma id_apply [simp]: "id x = x"
by (simp add: id_def)
-lemma image_id [simp]: "id ` Y = Y"
- by (simp add: id_def)
+lemma image_id [simp]: "image id = id"
+ by (simp add: id_def fun_eq_iff)
-lemma vimage_id [simp]: "id -` A = A"
- by (simp add: id_def)
+lemma vimage_id [simp]: "vimage id = id"
+ by (simp add: id_def fun_eq_iff)
subsection {* The Composition Operator @{text "f \<circ> g"} *}
--- a/src/HOL/Quotient.thy Thu Apr 19 11:10:03 2012 +0200
+++ b/src/HOL/Quotient.thy Thu Apr 19 10:49:47 2012 +0200
@@ -38,10 +38,6 @@
definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
-lemma vimage_id:
- "vimage id = id"
- unfolding vimage_def fun_eq_iff by auto
-
lemma set_rel_eq:
"set_rel op = = op ="
by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)