src/HOL/Hahn_Banach/Hahn_Banach.thy

     have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
     moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
     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 -
       have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>" by (simp only: p_def)
       also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)