src/HOL/Analysis/Vitali_Covering_Theorem.thy
changeset 67998 73a5a33486ee
parent 67996 6a9d1b31a7c5
child 68017 e99f9b3962bf
     1.1 --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Tue Apr 17 18:04:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Tue Apr 17 22:35:48 2018 +0100
     1.3 @@ -629,7 +629,6 @@
     1.4      by metis
     1.5  qed
     1.6  
     1.7 -
     1.8  proposition negligible_eq_zero_density:
     1.9     "negligible S \<longleftrightarrow>
    1.10      (\<forall>x\<in>S. \<forall>r>0. \<forall>e>0. \<exists>d. 0 < d \<and> d \<le> r \<and>