--- a/src/HOL/Hahn_Banach/Normed_Space.thy Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Mon Nov 02 11:43:02 2015 +0100
@@ -11,9 +11,9 @@
subsection \<open>Quasinorms\<close>
text \<open>
- A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space
- into the reals that has the following properties: it is positive
- definite, absolute homogeneous and subadditive.
+ A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals
+ that has the following properties: it is positive definite, absolute
+ homogeneous and subadditive.
\<close>
locale seminorm =