1.1 --- a/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:06:22 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:12:27 2012 +0200
     1.3 @@ -174,17 +174,6 @@
     1.4  
     1.5  subsection {* Setup for lifting package *}
     1.6  
     1.7 -lemma Quotient_alt_def3:
     1.8 -  "Quotient R Abs Rep T \<longleftrightarrow>
     1.9 -    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
    1.10 -    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
    1.11 -  unfolding Quotient_alt_def2 by (safe, metis+)
    1.12 -
    1.13 -lemma Quotient_alt_def4:
    1.14 -  "Quotient R Abs Rep T \<longleftrightarrow>
    1.15 -    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
    1.16 -  unfolding Quotient_alt_def3 fun_eq_iff by auto
    1.17 -
    1.18  lemma Quotient_set:
    1.19    assumes "Quotient R Abs Rep T"
    1.20    shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"