1.1 --- a/src/HOL/Set.thy	Sat Dec 17 12:51:30 2011 +0100
     1.2 +++ b/src/HOL/Set.thy	Sat Dec 17 13:08:03 2011 +0100
     1.3 @@ -1560,9 +1560,6 @@
     1.4  lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
     1.5    by blast
     1.6  
     1.7 -lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
     1.8 -  by iprover
     1.9 -
    1.10  lemma ball_simps [simp, no_atp]:
    1.11    "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
    1.12    "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
    1.13 @@ -1796,7 +1793,6 @@
    1.14  val bex_triv = @{thm bex_triv}
    1.15  val bspec = @{thm bspec}
    1.16  val contra_subsetD = @{thm contra_subsetD}
    1.17 -val distinct_lemma = @{thm distinct_lemma}
    1.18  val equalityCE = @{thm equalityCE}
    1.19  val equalityD1 = @{thm equalityD1}
    1.20  val equalityD2 = @{thm equalityD2}