--- a/src/HOL/Analysis/Continuous_Extension.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy Sun May 20 11:57:17 2018 +0200
@@ -298,7 +298,7 @@
subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
-http://projecteuclid.org/euclid.pjm/1103052106\<close>
+https://projecteuclid.org/euclid.pjm/1103052106\<close>
theorem%important Dugundji:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"