--- a/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -9,8 +9,8 @@
 begin
 
 text \<open>
-  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
-  that is additive and multiplicative.
+  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
+  additive and multiplicative.
 \<close>
 
 locale linearform =