--- a/src/HOL/Library/Extended_Real.thy Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Library/Extended_Real.thy Wed Mar 16 13:57:06 2016 +0000
@@ -12,15 +12,8 @@
imports Complex_Main Extended_Nat Liminf_Limsup
begin
-text \<open>
-
-This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
-AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.
-
-\<close>
-
-lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
- by auto
+text \<open>This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
+AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.\<close>
lemma incseq_setsumI2:
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add"