diff -r 8e4f50afd21a -r 1b722b100301 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:06:22 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:12:27 2012 +0200
@@ -174,17 +174,6 @@
 
 subsection {* Setup for lifting package *}
 
-lemma Quotient_alt_def3:
-  "Quotient R Abs Rep T \<longleftrightarrow>
-    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
-    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
-  unfolding Quotient_alt_def2 by (safe, metis+)
-
-lemma Quotient_alt_def4:
-  "Quotient R Abs Rep T \<longleftrightarrow>
-    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
-  unfolding Quotient_alt_def3 fun_eq_iff by auto
-
 lemma Quotient_set:
   assumes "Quotient R Abs Rep T"
   shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"