src/HOL/Hahn_Banach/Hahn_Banach.thy

 text \<open>
   Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
   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>
   \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
   of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.