Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Vitali_Covering_Theorem.thy
changeset 67998 73a5a33486ee
parent 67996 6a9d1b31a7c5
child 68017 e99f9b3962bf 
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Tue Apr 17 18:04:49 2018 +0100
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Tue Apr 17 22:35:48 2018 +0100
@@ -629,7 +629,6 @@
     by metis
 qed
 
-
 proposition negligible_eq_zero_density:
    "negligible S \<longleftrightarrow>
     (\<forall>x\<in>S. \<forall>r>0. \<forall>e>0. \<exists>d. 0 < d \<and> d \<le> r \<and>
isabelle