src/HOL/Real/HahnBanach/HahnBanach.thy

   norm space @{text E}, can be extended to a continuous linear form
   @{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}.
 *}
 
 theorem norm_HahnBanach:
-  includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm f
+  includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm ("\<parallel>_\<parallel>") f
   shows "\<exists>g. linearform E g
      \<and> continuous E norm g
      \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -