diff -r 10cfaf771687 -r f7b1034cb9ce src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Apr 20 15:30:13 2012 +0200
+++ b/src/HOL/Quotient.thy	Fri Apr 20 15:34:33 2012 +0200
@@ -34,21 +34,6 @@
   shows "((op =) OOO R) = R"
   by (auto simp add: fun_eq_iff)
 
-subsection {* set map (vimage) and set relation *}
-
-definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
-
-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)
-
-lemma set_rel_equivp:
-  assumes e: "equivp R"
-  shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
-  unfolding set_rel_def
-  using equivp_reflp[OF e]
-  by auto (metis, metis equivp_symp[OF e])
-
 subsection {* Quotient Predicate *}
 
 definition
@@ -799,7 +784,6 @@
   id_o
   o_id
   eq_comp_r
-  set_rel_eq
   vimage_id
 
 text {* Translation functions for the lifting process. *}