diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Continuous_Extension.thy
--- 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>