--- a/src/HOL/Probability/Levy.thy Thu Oct 13 18:36:06 2016 +0200
+++ b/src/HOL/Probability/Levy.thy Tue Oct 18 12:01:54 2016 +0200
@@ -8,11 +8,6 @@
imports Characteristic_Functions Helly_Selection Sinc_Integral
begin
-lemma LIM_zero_cancel:
- fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
- shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F"
-unfolding tendsto_iff dist_norm by simp
-
subsection \<open>The Levy inversion theorem\<close>
(* Actually, this is not needed for us -- but it is useful for other purposes. (See Billingsley.) *)