diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Analysis/Continuous_Extension.thy --- a/src/HOL/Analysis/Continuous_Extension.thy Sun Oct 02 13:47:39 2016 +0200 +++ b/src/HOL/Analysis/Continuous_Extension.thy Sun Oct 02 14:07:43 2016 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Analysis/Extension.thy +(* Title: HOL/Analysis/Continuous_Extension.thy Authors: LC Paulson, based on material from HOL Light *)