src/HOL/Analysis/Vitali_Covering_Theorem.thy

--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri Apr 20 19:11:17 2018 +0100
@@ -1,3 +1,9 @@
+(*  Title:      HOL/Analysis/Vitali_Covering_Theorem.thy
+    Authors:    LC Paulson, based on material from HOL Light
+*)
+
+section\<open>Vitali Covering Theorem and an Application to Negligibility\<close>
+
 theory Vitali_Covering_Theorem
   imports Ball_Volume "HOL-Library.Permutations"