--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Sat Apr 26 14:00:49 2014 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Sat Apr 26 14:01:06 2014 +0200
@@ -391,7 +391,7 @@
ultimately show "0 \<le> p x"
by (simp add: p_def zero_le_mult_iff)
- txt {* @{text p} is absolutely homogenous: *}
+ txt {* @{text p} is absolutely homogeneous: *}
show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
proof -
--- a/src/HOL/Hahn_Banach/Normed_Space.thy Sat Apr 26 14:00:49 2014 +0200
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Sat Apr 26 14:01:06 2014 +0200
@@ -13,7 +13,7 @@
text {*
A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
into the reals that has the following properties: it is positive
- definite, absolute homogenous and subadditive.
+ definite, absolute homogeneous and subadditive.
*}
locale seminorm =