--- a/src/HOL/Analysis/Continuous_Extension.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy Mon Apr 09 16:20:23 2018 +0200
@@ -295,7 +295,7 @@
using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
-subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
+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>