src/HOL/Hahn_Banach/Hahn_Banach.thy

   fixes V and norm ("\<parallel>_\<parallel>")
   fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
   fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
   defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
   assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
-    and linearform: "linearform F f" and "continuous F norm f"
+    and linearform: "linearform F f" and "continuous F f norm"
   shows "\<exists>g. linearform E g
-     \<and> continuous E norm g
+     \<and> continuous E g norm
      \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -
   interpret normed_vectorspace E norm by fact
   interpret normed_vectorspace_with_fn_norm E norm B fn_norm
     by (auto simp: B_def fn_norm_def) intro_locales
   interpret subspace F E by fact
   interpret linearform F f by fact
-  interpret continuous F norm f by fact
+  interpret continuous F f norm by fact
   have E: "vectorspace E" by intro_locales
   have F: "vectorspace F" by rule intro_locales
   have F_norm: "normed_vectorspace F norm"
     using FE E_norm by (rule subspace_normed_vs)
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
     by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
       [OF normed_vectorspace_with_fn_norm.intro,
-       OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
+       OF F_norm `continuous F f norm` , folded B_def fn_norm_def])
   txt {* We define a function @{text p} on @{text E} as follows:
     @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
   def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
 
   txt {* @{text p} is a seminorm on @{text E}: *}

   txt {* @{text f} is bounded by @{text p}. *}
 
   have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   proof
     fix x assume "x \<in> F"
-    with `continuous F norm f` and linearform
+    with `continuous F f norm` and linearform
     show "\<bar>f x\<bar> \<le> p x"
       unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
         [OF normed_vectorspace_with_fn_norm.intro,
          OF F_norm, folded B_def fn_norm_def])
   qed

     and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
     by (rule abs_Hahn_Banach [elim_format]) iprover
 
   txt {* We furthermore have to show that @{text g} is also continuous: *}
 
-  have g_cont: "continuous E norm g" using linearformE
+  have g_cont: "continuous E g norm" using linearformE
   proof
     fix x assume "x \<in> E"
     with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
       by (simp only: p_def)
   qed

         finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
       qed
       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
         using g_cont
         by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
-      show "continuous F norm f" by fact
+      show "continuous F f norm" by fact
     qed
   qed
   with linearformE a g_cont show ?thesis by blast
 qed