diff -r b3eb789616c3 -r de44d4fa5ef0 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 14:09:14 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 16:02:32 2015 +0100
@@ -22,7 +22,8 @@
   on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
   by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
   form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
-  by \<open>p\<close>. \<close>
+  by \<open>p\<close>.
+\<close>
 
 paragraph \<open>Proof Sketch.\<close>
 text \<open>